Perpetuality in a named lambda calculus with explicit substitutions

Research output: Contribution to journalArticlepeer-review

11 Scopus citations

Abstract

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

Original languageEnglish
Pages (from-to)47-90
Number of pages44
JournalMathematical Structures in Computer Science
Volume11
Issue number1
DOIs
StatePublished - 2001

Fingerprint

Dive into the research topics of 'Perpetuality in a named lambda calculus with explicit substitutions'. Together they form a unique fingerprint.

Cite this