Strong normalization proofs by CPS-translations

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

Satoshi Ikeda, Koji Nakazawa

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 normalization; programming calculi; permutative conversion; classical natural deduction; continuation passing style translation

Mathematics Subject Classification ID

68N18: Functional programming and lambda calculus

03B40: Combinatory logic and lambda calculus

Related Items

Strong cut-elimination in sequent calculus using Klop's ι-translation and perpetual reductions, Monadic Translation of Intuitionistic Sequent Calculus

Cites Work

• 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
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item