Title: | Automatic Generation of CINNI Instances for the Maude System |
Author(s): | Eckhardt, Jonas; Muelbauer, Tobias; Meseguer, José |
Subject(s): | higher-order syntax, explicit substitution, CINNI, Maude |
Abstract: | Many formal languages use the concept of names to range over essential
entities of the language and are usually equipped with special binding
constructs for names. For example, the lambda-calculus uses variables as names
and lambda-abstractions as a name binders; Milners pi-calculus uses the action
pre fixes in and new to bind variables in a subsequent term; and first-order
logic uses variables as names, which can be bound by the universal and existential
quantifiers. CINNI is a calculus of explicit substitutions that contributes a
first-order representation of terms which takes variable bindings into account
and captures free substitutions. The CINNI calculus is parametric in the
syntax of the object language, which allows it to be applied to many
di fferent object languages. The createCINNI tool makes the parametric nature of CINNI available
to the Maude system by means of an automatic module transformation which --given a Maude module specifying the syntax of an object
language L-- generates a Maude module containing the instantiation CINNI(L). |
Issue Date: | 2011-09-27 |
Genre: | Technical Report |
Type: | Text |
Language: | English |
URI: | http://hdl.handle.net/2142/27681 |
Publication Status: | unpublished |
Peer Reviewed: | not peer reviewed |
Sponsor: | NSF Grant CCF 09-05584 |
Rights Information: | Copyright 2011 by Jonas Eckhardt, Tobias Muelbauer and Jose Meseguer |
Date Available in IDEALS: | 2011-09-27 |