A formalised first-order confluence proof for the -calculus using one-sorted variable names.
From MaRDI portal
Publication:1401936
Recommendations
- scientific article; zbMATH DE number 1722714
- A coinductive confluence proof for infinitary lambda-calculus
- A new coinductive confluence proof for infinitary lambda calculus
- Confluence via strong normalisation in an algebraic -calculus with rewriting
- Confluence of the coinductive \(\lambda\)-calculus
- scientific article; zbMATH DE number 1499104
- Foundations of Software Science and Computation Structures
- Types for Proofs and Programs
- scientific article; zbMATH DE number 1140686
- A Nominal Axiomatization of the Lambda Calculus
Cites work
- A mechanical proof of the Church-Rosser theorem
- A new approach to abstract syntax with variable binding
- An algebraic interpretation of the K-calculus; and an application of a labelled -calculus
- Completion of a Set of Rules Modulo a Set of Equations
- scientific article; zbMATH DE number 1722714 (Why is no real title available?)
- scientific article; zbMATH DE number 3730111 (Why is no real title available?)
- scientific article; zbMATH DE number 482822 (Why is no real title available?)
- scientific article; zbMATH DE number 1538035 (Why is no real title available?)
- scientific article; zbMATH DE number 1841811 (Why is no real title available?)
- scientific article; zbMATH DE number 3280068 (Why is no real title available?)
- scientific article; zbMATH DE number 3400430 (Why is no real title available?)
- More Church-Rosser proofs (in Isabelle/HOL)
- Operational techniques in PVS -- a preliminary evaluation
- Parallel reductions in \(\lambda\)-calculus
- Primitive recursion for higher-order abstract syntax
- Proving Properties of Programs by Structural Induction
- Residual theory in λ-calculus: a formal development
- Some lambda calculus and type theory formalized
- Some Properties of Conversion
- Substitution revisited
- The lambda calculus. Its syntax and semantics. Rev. ed.
- The mechanisation of Barendregt-style equational proofs (the residual perspective)
Cited in
(13)- Formal metatheory of the lambda calculus using Stoughton's substitution
- scientific article; zbMATH DE number 1722714 (Why is no real title available?)
- The mechanisation of Barendregt-style equational proofs (the residual perspective)
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
- Proof pearl: Abella formalization of \(\lambda \)-calculus cube property
- Formalization of metatheory of the Lambda Calculus in constructive type theory using the Barendregt variable convention
- Formalisation in constructive type theory of Stoughton's substitution for the lambda calculus
- Completeness and Herbrand theorems for nominal logic
- \(\rightthreetimes\)
- Ground confluence and strong commutation modulo alpha-equivalence in nominal rewriting
- Formalization in constructive type theory of the standardization theorem for the lambda calculus using multiple substitution
- Barendregt's theory of the -calculus, refreshed and formalized
- Mechanising \(\lambda\)-calculus using a classical first order theory of terms with permutations
This page was built for publication: A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names.
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1401936)
