Strong normalization proof with CPS-translation for second order classical natural deduction

DOI10.2178/jsl/1058448444zbMath1058.03060OpenAlexW2128981898MaRDI QIDQ4650260

Makoto Tatsuta, Koji Nakazawa

Publication date: 9 February 2005

Published in: Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL: https://projecteuclid.org/euclid.jsl/1058448444

zbMATH Keywords

augmentationstrong normalizationCPS-translationsecond-order classical natural deduction

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Combinatory logic and lambda calculus (03B40)

Related Items (4)

Strong normalization proofs by CPS-translations ⋮ Unnamed Item ⋮ Monadic translation of classical sequent calculus ⋮ Strong normalization of classical natural deduction with disjunctions

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Confluency and strong normalizability of call-by-value \(\lambda \mu\)-calculus
• Domain-Freeλµ-Calculus

This page was built for publication: Strong normalization proof with CPS-translation for second order classical natural deduction