CINNI - A Generic Calculus of Explicit Substitutions and its Application to λ- ς- and π-Calculi Export

@article{citeulike:3484566, abstract = {We approach the general problem of representing higher-order languages, that are usually equipped with special variable binding constructs, in a less specialized first-order framework such as membership equational logic and the corresponding version of rewriting logic. The solution we propose is based on CINNI, a new calculus of explicit substitutions that makes use of a term representation that contains both the standard named notation and de Bruijn's indexed notation as special subcases. The calculus is parametric in the syntax of the object language, which allows us to apply it to different object languages such as \&\#x3bb;-calculus, Abadi and Cardelli's object calculus (\&\#x3c2;-calculus) and Milner's calculus of communicating mobile processes (\&\#x3c0;-calculus). As a practical result we obtain executable formal representations of these object languages in Maude with a representational distance close to zero.}, author = {Oliverstehr, M.}, citeulike-article-id = {3484566}, citeulike-linkout-0 = {http://dx.doi.org/10.1016/S1571-0661(05)80125-2}, citeulike-linkout-1 = {http://linkinghub.elsevier.com/retrieve/pii/S1571066105801252}, doi = {10.1016/S1571-0661(05)80125-2}, issn = {15710661}, journal = {Electronic Notes in Theoretical Computer Science}, keywords = {maude, termrewriting}, pages = {70--92}, posted-at = {2008-11-06 14:16:59}, priority = {0}, title = {CINNI - A Generic Calculus of Explicit Substitutions and its Application to λ- ς- and π-Calculi}, url = {http://dx.doi.org/10.1016/S1571-0661(05)80125-2}, volume = {36}, year = {2000} }

TY - JOUR ID - citeulike:3484566 L3 - citeulike-article-id:3484566 N2 - We approach the general problem of representing higher-order languages, that are usually equipped with special variable binding constructs, in a less specialized first-order framework such as membership equational logic and the corresponding version of rewriting logic. The solution we propose is based on CINNI, a new calculus of explicit substitutions that makes use of a term representation that contains both the standard named notation and de Bruijn's indexed notation as special subcases. The calculus is parametric in the syntax of the object language, which allows us to apply it to different object languages such as λ-calculus, Abadi and Cardelli's object calculus (ς-calculus) and Milner's calculus of communicating mobile processes (π-calculus). As a practical result we obtain executable formal representations of these object languages in Maude with a representational distance close to zero. JF - Electronic Notes in Theoretical Computer Science SN - 15710661 EP - 92 TI - CINNI - A Generic Calculus of Explicit Substitutions and its Application to λ- ς- and π-Calculi VL - 36 SP - 70 KW - maude KW - termrewriting AU - Oliverstehr, M PY - 2000/// UR - http://dx.doi.org/10.1016/S1571-0661(05)80125-2 ER -