Compositional Z: confluence proofs for permutative conversion

DOI10.1007/S11225-016-9673-0zbMATH Open1368.03020OpenAlexW2407924833WikidataQ113900501 ScholiaQ113900501MaRDI 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

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

zbMATH Keywords

confluencelambda calculuslambda-mu calculuspermutative conversion

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Some Properties of Conversion
• Parallel reduction in type free lambda/mu-calculus
• Confluence of extensional and non-extensional \(\lambda\)-calculi with explicit substitutions
• Church-Rosser property of a simple reduction for full first-order classical natural deduction
• A simplified proof of the Church-Rosser theorem
• Call-by-name reduction and cut-elimination in classical logic
• The permutative \(\lambda \)-calculus
• Reduction System for Extensional Lambda-mu Calculus
• Parallel reductions in \(\lambda\)-calculus

Cited In (6)

• A formal system of reduction paths for parallel reduction
• Title not available (Why is that?)
• The permutative \(\lambda \)-calculus
• The Church-Rosser theorem and quantitative analysis of witnesses
• Z property for the shuffling calculus
• Confluence proofs of lambda-mu-calculi by Z theorem

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)