Residual theory in λ-calculus: a formal development

DOI10.1017/S0956796800001106zbMath0826.03008OpenAlexW1496085154MaRDI QIDQ4764621

Gérard Huet

Publication date: 28 November 1995

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

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

zbMATH Keywords

confluencecalculus of inductive constructionsLévy cube lemmaparallel-moves lemmaprism theoremresidual theory of \(\beta\)-reduction

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40)

Related Items

Upper bounds for standardizations and an application, Mechanising \(\lambda\)-calculus using a classical first order theory of terms with permutations, More Church-Rosser proofs (in Isabelle/HOL), Developing developments, A formalization of the Knuth-Bendix(-Huet) critical pair theorem, Braids via term rewriting, A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names., Variable binding and substitution for (nameless) dummies, A solution to the PoplMark challenge using de Bruijn indices in Isabelle/HOL, A solution to the PoplMark challenge based on de Bruijn indices, Development closed critical pairs, Proof Pearl: Abella Formalization of λ-Calculus Cube Property, A PVS Theory for Term Rewriting Systems, Proof-relevant π-calculus: a constructive account of concurrency and causality, The Mechanisation of Barendregt-Style Equational Proofs (the Residual Perspective), A Formalisation of Weak Normalisation (with Respect to Permutations) of Sequent Calculus Proofs, A note on subject reduction in \((\to, \exists)\)-Curry with respect to complete developments, The practice of logical frameworks

Uses Software

• Coq
• IMPS
• Gallina

Cites Work

• The lambda calculus. Its syntax and semantics. Rev. ed.