Automatic Generation of CINNI Instances for the Maude System

Eckhardt, Jonas; Muelbauer, Tobias; Meseguer, José

Permalink

https://hdl.handle.net/2142/27681 Copy

Description

Title

Automatic Generation of CINNI Instances for the Maude System

Author(s)

• Eckhardt, Jonas
• Muelbauer, Tobias
• Meseguer, José

Issue Date

2011-09-27

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

Type of Resource

text

Language

en

Permalink

http://hdl.handle.net/2142/27681

Sponsor(s)/Grant Number(s)

NSF Grant CCF 09-05584

Copyright and License Information

Copyright 2011 by Jonas Eckhardt, Tobias Muelbauer and Jose Meseguer

Owning Collections