Automatic Generation of CINNI Instances for the Maude System

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).