Hostname: page-component-74656f9884-rdgjk Total loading time: 0 Render date: 2026-11-09T12:28:05.205Z Has data issue: false hasContentIssue false

Perpetuality in a named lambda calculus with explicit substitutions

Published online by Cambridge University Press:  07 March 2001

EDUARDO BONELLI
Affiliation:
Laboratoire de Recherche en Informatique, Bât 490, Université de Paris-Sud, 91405, Orsay Cedex, France. Email: bonelli@lri.fr Departamento de Computación, Facultad de Ciencias Exactas y Naturales, Universidad de Buenos Aires, Argentina.
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

We study perpetuality in the calculus of explicit substitutions λx. A reduction is called perpetual if it preserves the possibility of infinite reduction sequences. We then take a look at applications of this study: an inductive characterization of the λx-strongly normalizing terms, two perpetual reduction strategies for λx and finally a proof of strong normalization of a polymorphic lambda calculus with explicit substitutions Fes. To complete the study of Fes, the property of subject reduction is shown to hold by extending type assignments of the typing rules to allow non-pure types (types with possible occurrences of the type substitution operator).

Information

Type
Research Article
Copyright
© 2001 Cambridge University Press