Simplified reducibility proofs of Church-Rosser for - and -reduction

DOI10.1016/J.ENTCS.2009.07.050MaRDI QIDQ5178963zbMATH OpenOpenAlexFDO

Authors Fairouz Kamareddine, Vincent Rahli

Publication date 18 March 2015

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2009.07.050

zbMATH Keywords

Church-Rosser propertyparallel reductionsreducibility

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Recommendations

• Reducibility Proofs in the λ-Calculus
• Church–Rosser Made Easy
• More Church-Rosser proofs (in Isabelle/HOL)
• More Church-Rosser proofs (in Isabelle/HOL)
• scientific article; zbMATH DE number 5558176

Cites work

• A formulation of the simple theory of types
• An algebraic interpretation of the K-calculus; and an application of a labelled -calculus
• Church-Rosser theorem for typed functional systems
• scientific article; zbMATH DE number 5558176 (Why is no real title available?)
• scientific article; zbMATH DE number 46869 (Why is no real title available?)
• scientific article; zbMATH DE number 177773 (Why is no real title available?)
• scientific article; zbMATH DE number 3619856 (Why is no real title available?)
• scientific article; zbMATH DE number 2044492 (Why is no real title available?)
• Intensional interpretations of functionals of finite type I
• On the interpretation of intuitionistic number theory
• Parallel reductions in \(\lambda\)-calculus
• Reducibility Proofs in the λ-Calculus
• Reductions of Residuals are Finite
• Some Properties of Conversion
• The lambda calculus. Its syntax and semantics. Rev. ed.

Cited in

(4)

• More Church-Rosser proofs (in Isabelle/HOL)
• On the Church-Rosser property and reducibility of natural derivations
• Church‐Rosser Property for Some Extensions of λβ‐Reducibility Relation
• Type inference and strong static type checking for Promela

Describes a project that uses

Uses Software

• Automath

This page was built for publication: Simplified reducibility proofs of Church-Rosser for \({\beta}\)- and \({\beta}{\eta}\)-reduction

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5178963)