Strong normalization proofs by CPS-translations

DOI10.1016/j.ipl.2006.03.009zbMath1185.68625OpenAlexW2041951938MaRDI QIDQ845711

Koji Nakazawa, Satoshi Ikeda

Publication date: 29 January 2010

Published in: Information Processing Letters (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ipl.2006.03.009

zbMATH Keywords

strong normalizationprogramming calculipermutative conversionclassical natural deductioncontinuation passing style translation

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Combinatory logic and lambda calculus (03B40)

Related Items (6)

Unnamed Item ⋮ Unnamed Item ⋮ Some properties of the -calculus ⋮ Monadic translation of classical sequent calculus ⋮ Strong cut-elimination in sequent calculus using Klop's ι-translation and perpetual reductions ⋮ Monadic Translation of Intuitionistic Sequent Calculus

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• On the strong normalisation of intuitionistic natural deduction with permutation-conversions
• Strong normalization from weak normalization by translation into the lambda-I-calculus
• Non-strictly positive fixed points for classical natural deduction
• Domain-Freeλµ-Calculus
• Proofs of strong normalisation for second order classical natural deduction
• Strong normalization proof with CPS-translation for second order classical natural deduction
• A short proof of the strong normalization of classical natural deduction with disjunction

This page was built for publication: Strong normalization proofs by CPS-translations