Extending a λ-calculus with explicit substitution which preserves strong normalisation into a confluent calculus on open terms

DOI10.1017/S0956796897002785zbMath0882.03011OpenAlexW2017143801MaRDI QIDQ4360125

Publication date: 12 March 1998

Published in: Journal of Functional Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0956796897002785

zbMATH Keywords

weak normalization $\lambda$-calculus strong normalization explicit substitution interpretation method confluent on open terms

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Combinatory logic and lambda calculus (03B40)

Related Items (10)

Intersection types for explicit substitutions ⋮ Unification for $$\lambda $$ -calculi Without Propagation Rules ⋮ Choices in representation and reduction strategies for lambda terms in intensional contexts ⋮ A useful $\lambda$-notation ⋮ The Suspension Notation for Lambda Terms and its Use in Metalanguage Implementations ⋮ Comparing Calculi of Explicit Substitutions with Eta-reduction ⋮ Explicit Substitutions à la de Bruijn ⋮ Comparing and implementing calculi of explicit substitutions with eta-reduction ⋮ SUBSEXPL: a tool for simulating and comparing explicit substitutions calculi ★ ⋮ THE SOUNDNESS OF EXPLICIT SUBSTITUTION WITH NAMELESS VARIABLES

This page was built for publication: Extending a λ-calculus with explicit substitution which preserves strong normalisation into a confluent calculus on open terms