Confluency and strong normalizability of call-by-value \(\lambda \mu\)-calculus

DOI10.1016/S0304-3975(01)00380-2zbMath1018.68016OpenAlexW1968553947MaRDI QIDQ1853595

Koji Nakazawa

Publication date: 21 January 2003

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0304-3975(01)00380-2

zbMATH Keywords

strong normalizabilitydomain-free type systemCPS-translationconfluencycall-by-value -calculus

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Related Items (4)

Strong normalization of the second-order symmetric \(\lambda \mu\)-calculus ⋮ Unnamed Item ⋮ Strong normalization proof with CPS-translation for second order classical natural deduction ⋮ Confluence proofs of lambda-mu-calculi by Z theorem

Uses Software

• Automath

Cites Work

• The system \({\mathcal F}\) of variable types, fifteen years later
• A syntactic theory of sequential control
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• A strong normalization result for classical logic
• Domain-Freeλµ-Calculus
• λμ-calculus and Böhm's theorem
• Proofs of strong normalisation for second order classical natural deduction
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Confluency and strong normalizability of call-by-value \(\lambda \mu\)-calculus