Confluence properties of weak and strong calculi of explicit substitutions

DOI10.1145/226643.226675zbMath0885.03014OpenAlexW1992452788MaRDI QIDQ4371674

Pierre-Louis Curien, Thérèse Hardin, Jean-Jacques Levy

Publication date: 21 January 1998

Published in: Journal of the ACM (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/inria-00077189/file/RR-1617.pdf

zbMATH Keywords

confluencecategorical combinatorscalculi of explicit substitutionsfunctional constructslambda-sigma-calculus

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) General topics in the theory of software (68N01) Combinatory logic and lambda calculus (03B40)

Related Items (26)

Unnamed Item ⋮ 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 ⋮ On explicit substitution with names ⋮ On explicit substitutions and names (extended abstract) ⋮ A syntactic correspondence between context-sensitive calculi and abstract machines ⋮ A \(\rho\)-calculus of explicit constraint application ⋮ Why Would You Trust B? ⋮ Formalization of a λ-calculus with explicit substitutions in Coq ⋮ Unnamed Item ⋮ Algebraic interpretation of lambda calculus with resources ⋮ Inter-deriving Semantic Artifacts for Object-Oriented Programming ⋮ Encoding the Pure Lambda Calculus into Hierarchical Graph Rewriting ⋮ Pure type systems with explicit substitutions ⋮ Theorem proving modulo ⋮ Strongly reducing variants of the Krivine abstract machine ⋮ Comparing Calculi of Explicit Substitutions with Eta-reduction ⋮ Inter-deriving semantic artifacts for object-oriented programming ⋮ Lambda-calculus with director strings ⋮ Comparing and implementing calculi of explicit substitutions with eta-reduction ⋮ Proof-term synthesis on dependent-type systems via explicit substitutions ⋮ The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: A proof via corresponding calculus ⋮ Normalization by Evaluation for Typed Weak lambda-Reduction ⋮ Certifying Term Rewriting Proofs in ELAN ⋮ Higher order unification via explicit substitutions ⋮ Strong normalization of substitutions

This page was built for publication: Confluence properties of weak and strong calculi of explicit substitutions