Normalization in the simply typed -calculus

DOI10.1017/S096012952200041XOpenAlexW4315701730MaRDI QIDQ5889885

Péter Battyányi, Karim Nour

Publication date: 27 April 2023

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s096012952200041x

zbMATH Keywords

weak normalizationstrong normalizationclassical logicnormalization algorithm\(\lambda\mu\)-calculus

Mathematics Subject Classification ID

Computer science (68-XX)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Böhm theorem and Böhm trees for the \(\varLambda \mu\)-calculus
• The value of a classical integer in \(\lambda \mu\)-calculus
• A completeness result for the simply typed \(\lambda \mu \)-calculus
• Lectures on the Curry-Howard isomorphism
• Classical logic, storage operators and second-order lambda-calculus
• Normalization proofs for the un-typed \(\mu\mu^\prime\)-calculus
• The duality of computation
• On the Relations between the Syntactic Theories of λμ-Calculi
• Arithmetical proofs of strong normalization results for symmetric lambda calculi
• An environment machine for the λμ-calculus
• Proofs of strong normalisation for second order classical natural deduction
• Non deterministic classical logic: the $\lambda\mu^{++}$-calculus
• Call-by-value is dual to call-by-name
• A revised completeness result for the simply typed $\lambda\mu$-calculus using realizability semantics
• Term Rewriting and Applications
• Typed Lambda Calculi and Applications

This page was built for publication: Normalization in the simply typed -calculus