Files in this item



application/pdfcreateCINNI.pdf (357kB)
(no description provided)PDF


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

This item appears in the following Collection(s)

Item Statistics