λν, a calculus of explicit substitutions which preserves strong normalisation

DOI10.1017/S0956796800001945zbMath0873.68108MaRDI QIDQ3125228

Daniel Briaud, Jocelyne Rouyer-Degli, Zine-El-Abidine Benaissa, Pierre Lescanne

Publication date: 29 April 1997

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

zbMATH Keywords

\(\lambda\)-calculus\(\lambda\sigma\)-calculus

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Grammars and rewriting systems (68Q42)

Related Items (27)

Pattern matching as cut elimination ⋮ Unnamed Item ⋮ Intersection types for explicit substitutions ⋮ Explicit substitutions with de bruijn's levels ⋮ Confluence properties of extensional and non-extensional λ-calculi with explicit substitutions (extended abstract) ⋮ On the enumeration of closures and environments with an application to random generation ⋮ Unification for $$\lambda $$ -calculi Without Propagation Rules ⋮ On explicit substitution with names ⋮ Choices in representation and reduction strategies for lambda terms in intensional contexts ⋮ Resource operators for \(\lambda\)-calculus ⋮ Revisiting the notion of function ⋮ A prismoid framework for languages with resources ⋮ 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 ⋮ Normalisation for higher-order calculi with explicit substitutions ⋮ Lambda-calculus with director strings ⋮ Comparing and implementing calculi of explicit substitutions with eta-reduction ⋮ Unnamed Item ⋮ Experimenting with Deduction Modulo ⋮ Strong Normalisation of Cut-Elimination That Simulates β-Reduction ⋮ A rewriting logic approach to operational semantics ⋮ Explicit substitution. On the edge of strong normalization ⋮ Confluence of extensional and non-extensional \(\lambda\)-calculi with explicit substitutions ⋮ A Rewriting Logic Approach to Operational Semantics (Extended Abstract) ⋮ Meta-programming With Built-in Type Equality ⋮ Equational rules for rewriting logic

Cites Work

• Unnamed Item
• The lambda calculus. Its syntax and semantics. Rev. ed.
• An abstract framework for environment machines
• Confluence results for the pure strong categorical logic CCL. \(\lambda\)- calculi as subsystems of CCL
• Categorical combinators
• ON STEPWISE EXPLICIT SUBSTITUTION
• Explicit substitutions

This page was built for publication: λν, a calculus of explicit substitutions which preserves strong normalisation