Summary

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 λ-calculus uses variables as names and λ-abstractions as a name binders; Milner’s π-calculus uses the action prefixes in and new to bind variables in a subsequent term; and first-order logic uses variables as names, which can be bound by the ∀ and ∃ quantifiers.

CINNI (Stehr) 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 different object languages. Stehr shows applications of CINNI to the λ-, ς-, and π-Calculi in Maude.

The createCINNI tool makes the parametric nature of CINNI available to Maude users 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 CINNIL.

Publications

Mark-Oliver Stehr
CINNI - A Generic Calculus of Explicit Substitutions and its Application to lambda-, sigma- and pi-calculi (2000)
Electronic Notes in Theoretical Computer Science, 36:70–92

Jonas Eckhardt, Tobias Mühlbauer, José Meseguer
Automatic Generation of CINNI Instances for the Maude System (2011)
Technical Report, University of Illinois at Urbana-Champaign, Download

Download

createCINNI with examples (gzip)

Requirements

Usage

./createCINNI.sh {module name} {substitution sort} {name sort} {indexed name sort} {value sort} {module file}
returns
CINNI-{module file}

About