We present a simple term language with explicit operators for erasure, duplication and substitution enjoying a sound and complete correspondence with the intuitionistic fragment of Linear Logic's Proof Nets. We establish the good operational behaviour of the language by means of some fundamental properties such as confluence, preservation of strong normalisation, strong normalisation of well-typed terms and step by step simulation. This formalism is the first term calculus with explicit substitutions having full composition and preserving strong normalisation. © Springer-Verlag Berlin Heidelberg 2005.
CITATION STYLE
Kesner, D., & Lengrand, S. (2005). Extending the explicit substitution paradigm. In Lecture Notes in Computer Science (Vol. 3467, pp. 407–422). Springer Verlag. https://doi.org/10.1007/978-3-540-32033-3_30
Mendeley helps you to discover research relevant for your work.