Compositional Z: confluence proofs for permutative conversion

DOI10.1007/S11225-016-9673-0zbMATH1368.03020OpenAlexW2407924833WikidataQ113900501MaRDI QIDQ514511FDOQ514511

Authors Koji Nakazawa, Ken-etsu Fujita

Publication date 2 March 2017

Published in Studia Logica (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s11225-016-9673-0

zbMATH Keywords

confluencelambda calculuslambda-mu calculuspermutative conversion

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Recommendations

• Z property for the shuffling calculus
• The permutative \(\lambda \)-calculus
• Termination of permutative conversions in intuitionistic Gentzen calculi
• scientific article; zbMATH DE number 1615235
• A direct proof of the confluence of combinatory strong reduction

Cites work

• scientific article; zbMATH DE number 1324438 (Why is no real title available?)
• scientific article; zbMATH DE number 3275554 (Why is no real title available?)
• A simplified proof of the Church-Rosser theorem
• Call-by-name reduction and cut-elimination in classical logic
• Church-Rosser property of a simple reduction for full first-order classical natural deduction
• Confluence of extensional and non-extensional \(\lambda\)-calculi with explicit substitutions
• Parallel reduction in type free lambda/mu-calculus
• Parallel reductions in \(\lambda\)-calculus
• Reduction system for extensional lambda-mu calculus
• Some Properties of Conversion
• The permutative \(\lambda \)-calculus

Cited in

(6)

• The permutative \(\lambda \)-calculus
• Z property for the shuffling calculus
• Confluence proofs of lambda-mu-calculi by Z theorem
• The Church-Rosser theorem and quantitative analysis of witnesses
• A formal system of reduction paths for parallel reduction
• scientific article; zbMATH DE number 1615235 (Why is no real title available?)

This page was built for publication: Compositional Z: confluence proofs for permutative conversion

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