Compositional Z: confluence proofs for permutative conversion
From MaRDI portal
Publication:514511
DOI10.1007/s11225-016-9673-0zbMath1368.03020OpenAlexW2407924833WikidataQ113900501 ScholiaQ113900501MaRDI QIDQ514511
Ken-etsu Fujita, Koji Nakazawa
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
Related Items
The Church-Rosser theorem and quantitative analysis of witnesses, A formal system of reduction paths for parallel reduction, Confluence proofs of lambda-mu-calculi by Z theorem, Z property for the shuffling calculus
Cites Work
- 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 λ-Calculus
- Reduction System for Extensional Lambda-mu Calculus
- Some Properties of Conversion
- Parallel reductions in \(\lambda\)-calculus
- Unnamed Item
- Unnamed Item
- Unnamed Item
