CINNI – a generic calculus of explicit substitutions and its application to \(\lambda\)-, \(\sigma\)- and \(\pi\)-calculi.

*(English)*Zbl 0966.68147
Futatsugi, Kokichi, The 3rd international workshop on rewriting logic and its applications, RWLW. Kanazawa City Cultural Hall, Kanzawa, Japan, September 18-20, 2000. Amsterdam: Elsevier, Electronic Notes in Theoretical Computer Science. 36, 23 p., electronic only (2000).

Summary: 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 \(\lambda\)-calculus, Abadi and Cardelli’s object calculus \(\varsigma\)-calculus) and Milner’s calculus of communicating mobile processes \(\pi\)-calculus. As a practical result we obtain executable formal representations of these object languages in Maude with a representational distance close to zero.

For the entire collection see [Zbl 0957.00046].

For the entire collection see [Zbl 0957.00046].

##### MSC:

68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |

##### Keywords:

rewriting logic
PDF
BibTeX
XML
Cite

\textit{M.-O. Stehr}, in: The 3rd international workshop on rewriting logic and its applications, RWLW. Kanazawa City Cultural Hall, Kanzawa, Japan, September 18--20, 2000. Amsterdam: Elsevier. 23 p. (2000; Zbl 0966.68147)

Full Text:
Link

##### References:

[1] | Abadi, M.; Cardelli, L.: A theory of objects. (1996) · Zbl 0876.68014 |

[2] | Abadi, M.; Cardelli, L.; Curien, P. -L.; Lévy, J. -J.: Explicit substitutions. Journal of functional programming 1, No. 4, 375-416 (1991) · Zbl 0941.68542 |

[3] | Barendregt, H. P.: Lambda-calculi with types. Background: computational structures, volume 2 of handbook of logic in computer science. (1992) |

[4] | Benaissa, Z.; Briaud, D.; Lescanne, P.; Rouyer-Degli, J.: \(\lambda\)v, a calculus of explicit substitutions which preserves strong normalisation. Journal of functional programming 6, No. 5, 699-722 (September 1996) · Zbl 0873.68108 |

[5] | Berardi, S.: Towards a mathematical analysis of the coquand-huet calculus of constructions and other systems in barendregt’s cube. Technical report, carnegie mellon university and universita di Torino (1988) |

[6] | Berkling, K. J.: A symmetric complement to the lambda-calulus. Technical report interner bericht ISF-76-7, GMD (1976) |

[7] | Berkling, K. J.; Fehr, E.: A consistent extension of the lambda-calculus as a base for functional programming languages. Information and control 55, 89-101 (1982) · Zbl 0553.68025 |

[8] | R. Bloo. Preservation of Termination for Explicit Substitution. PhD thesis, Eindhoven University of Technology, 1997. IPA Dissertation Series 1997-05. · Zbl 0883.03008 |

[9] | Bloo, R.; Rose, K. H.: Combinatory reduction systems with explicit substitution that preserve strong normalisation. RTA ’96-rewriting techniques and applications, New Brunswick, new jersey, July 1996, rutgers university, volume 1103 of lecture notes in computer science, 169-183 (1996) |

[10] | Bouhoula, A.; Jouannaud, J. -P.; Meseguer, J.: Specification and proof in membership equational logic. Theoretical computer science 236, 35-132 (2000) · Zbl 0938.68057 |

[11] | M. Clavel, F. Dur\'n, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, and J. Quesada. A tutorial on Maude. SRI International, March 2000, http://maude.csl.sri.com. · Zbl 0962.68108 |

[12] | Clavel, M.; Duran, F.; Eker, S.; Lincoln, P.; Martí-Oliet, N.; Meseguer, J.; Quesada, J.: Maude: specification and programming in rewriting logic. (1999) · Zbl 0962.68108 |

[13] | Coquand, T.; Huet, G.: The calculus of constructions. Information and computation 76(2/3), 95-120 (1988) · Zbl 0654.03045 |

[14] | Curien, P. -L.: An abstract framework for environment machines. Theoretical computer science 82, 389-402 (1991) · Zbl 0727.68033 |

[15] | Curien, P. -L.; Hardin, T.; Lévy, J. -J.: Confluence properties of weak and strong calculi of explicit substitutions. Journal of the ACM 43, No. 2, 362-397 (1996) · Zbl 0885.03014 |

[16] | De Bruijn, N. G.: Lambda calculus with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem. In proc. Kninkl. nederl. Akademie Van wetenschappen 75, No. 5, 381-392 (1972) · Zbl 0253.68007 |

[17] | G. Dowek, T. Hardin, and C. Kirchner. Higher-order unification via explicit substitutions. In D. Kozen, editor, Proceedings of the Tenth Annual Symposium on Logic in Computer Science, San Diego, California, June 1995, pages 366-374. IEEE Computer Society Press, 1995. · Zbl 1005.03016 |

[18] | G. Dowek, T. Hardin, and C. Kirchner. HOL-lambda-sigma: An intentional first-order expression of higher-order logic. In P. Narendran and M. Rusinowitch, editors, Proceedings of the 10th International Conference on Rewriting Techniques and Applications (RTA-99), Trento, Italy, July 1999, volume 1631 of Lecture Notes in Computer Science, pages 317-331. Springer-Verlag, 1999. · Zbl 0944.03007 |

[19] | J. Field. On laziness and optimality in lambda interpreters: Tools for specification and analysis. In Proceedings of the 17th Anual ACM Symposium on Principles of Programming Languages, Orlando (Florida, USA), pages 1-15. ACM, San Francisco, 1990. |

[20] | Hardin, T.: Confluence results for the pure strong categorical combinatory logic. Theoretical computer science (1988) |

[21] | D. Hirschkoff. Handling substitutions explicitely in the pi-calculus. In Proceedings of WESTAPP’99, Second International Workshop on Explicit Substitutions: Theory and Applications to Programs and Proofs, July 5, 1999, Trento, Italy. |

[22] | Kamareddine, F.; Ríos, A.: Relating the \({\lambda}{\sigma}\) and \({\lambda}\)s-styles of explicit substitutions. Journal of logic and computation (2000) · Zbl 0953.03013 |

[23] | Kesner, D.; López, P. E. M.: Explicit substitutions for objects and functions. The journal of functional and logic programming (1999) |

[24] | P. Lescanne. Termination of rewrite systems by elementary interpretations. In H. Kirchner and G. Levi, editors, Algebraic and Logic Programming, Third International Conference, Volterra, Italy, September 1992, Proceedings, volume 632 of Lecture Notes in Computer Science, pages 21 - 36. Springer-Verlag, 1992. |

[25] | P. Lescanne. From \(\lambda\)\(\sigma\) to \(\lambda\)v, a journey through calculi of explicit substitutions. In Hans Boehm, editor, Proc. 21st Annual ACM Synposium on Principles of Programming Languages, Portland, USA, pages 60-69. ACM, 1994. |

[26] | P. Lescanne and J. Rouyer-Degli. The calculus of explicit substitutions \(\lambda\)v. Technical Report RR-2222, INRIA-Lorraine, January 1994. |

[27] | Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical computer science 96, 73-155 (1992) · Zbl 0758.68043 |

[28] | Meseguer, J.: Membership algebra as a logical framework for equational specification. Recent trends in algebraic development techniques, 12th international workshop, WADT ’97, tarquinia, Italy, June 3-7, 1997, selected papers, volume 1376 of lecture notes in computer science, 18-61 (1998) · Zbl 0903.08009 |

[29] | Milner, R.: Communicating and mobile systems: the pi-calculus. (May 1999) · Zbl 0942.68002 |

[30] | Muñoz, C.: A calculus of substitutions for incomplete-proof representation in type theory. Technical report RR-3309, unité de recherche INRIA-Rocquencourt (Novembre 1997) |

[31] | C. Muñoz. Proof synthesis via explicit substitutions on open terms. In Proc. International Workshop on Explicit Substitutions, Theory and Applications, WESTAPP 98, Tsukuba (Japan), April 1998. |

[32] | O’donnell, M. J.: Computing in systems descibed by equations. (1977) |

[33] | B. Pagano. X.R.S.: Explicit reduction systems - a first-order calculus for higher-order calculi. In C. Kirchner and H. Kirchner, editors, Automated Deduction - CADE-15, 15th International Conference on Automated Deduction, Lindau, Germany, July 1998, Proceedings, volume 1421 of Lecture Notes in Artificial Intelligence. Springer-Verlag, 1998. · Zbl 0924.03047 |

[34] | C. Reinke. Functions, Frames and Interactions - completing a \(\lambda\)-calculus-based purely functional language with respect to programming-in-the-large and interactions with runtime environments. PhD thesis, Christian-Albrechts-Universität Kiel, Germany, 1998. Report 9804. · Zbl 0924.68033 |

[35] | Rose, K. H.: Explicit substitution - tutorial & survey. Technical report lecture series LS-96-3, BRICS, dept.. Of computer science, university of Aarhus (September 1996) |

[36] | M.-O. Stehr and J. Meseguer. Pure type systems in rewriting logic. In Proc. of LFM’99: Workshop on Logical Frameworks and Meta-languages, Paris, France, September 28, 1999. |

[37] | M.O. Stehr. CINNI - A Generic Calculus of Explicit Substitutions and its Application to lambda-, sigma- and pi-calculi. Extended version of this paper available at http://www.csl.sri/ stehr, October 2000. · Zbl 0966.68147 |

[38] | Terlouw, J.: Een nadere bewijstheoretische analyse Van gstts. (1989) |

[39] | P. Viry. Input/output for ELAN. In J. Meseguer, editor, Proceedings of the 1st International Workshop on Rewriting Logic and its Applications, Asilomar, California, September 1996, volume 4 of Electronic Notes in Theoretical Computer Science. Elsevier, 1996. http://www.elsevier.com/locate/entcs/volume4.html. · Zbl 0912.68093 |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.