Choices in representation and reduction strategies for lambda terms in intensional contexts

DOI10.1007/s10817-004-6885-1zbMath1102.68019OpenAlexW2092768924MaRDI QIDQ861365

Gopalan Nadathur, Chuck Liang, Xiaochu Qi

Publication date: 29 January 2007

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-004-6885-1

zbMATH Keywords

implementationlambda calculusexplicit substitutionlambda conversion

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40)

Related Items

A \(\rho\)-calculus of explicit constraint application ⋮ Higher-order unification: a structural relation between Huet's method and the one based on explicit substitutions ⋮ SUBSEXPL: a tool for simulating and comparing explicit substitutions calculi ★ ⋮ Mechanized metatheory revisited

Uses Software

• Coq
• Isabelle/HOL
• Prolog
• Nuprl
• Twelf
• Automath
• Teyjus

Cites Work

• Unnamed Item
• Unnamed Item
• The calculus of constructions
• A notation for lambda terms. A generalization of environments
• An efficient interpreter for the lambda-calculus
• Unification under a mixed prefix
• A unification algorithm for typed \(\overline\lambda\)-calculus
• Isabelle/HOL. A proof assistant for higher-order logic
• Higher order unification via explicit substitutions
• A λ-calculus with explicit weakening and explicit substitution
• A compiled implementation of strong reduction
• λν, a calculus of explicit substitutions which preserves strong normalisation
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• A framework for defining logics
• Extending a λ-calculus with explicit substitution which preserves strong normalisation into a confluent calculus on open terms
• Closed reduction: explicit substitutions without $\alpha$ -conversion
• Explicit substitutions