On the strong normalisation of intuitionistic natural deduction with permutation-conversions

DOI10.1006/inco.2002.3147zbMath1031.03071OpenAlexW1995083622MaRDI QIDQ1400711

Philippe de Groote

Publication date: 4 March 2004

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://semanticscholar.org/paper/45e96e9ce1d9e30a167f403c71f3143795b5b187

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05)

Related Items (7)

Strong normalization proofs by CPS-translations ⋮ Intuitionistic games: determinacy, completeness, and normalization ⋮ Strong normalization of classical natural deduction with disjunctions ⋮ Unnamed Item ⋮ Curry-Howard-Lambek correspondence for intuitionistic belief ⋮ Natural deduction systems for Nelson's paraconsistent logic and its neighbors ⋮ A simple proof of second-order strong normalization with permutative conversions

Cites Work

• The lambda calculus. Its syntax and semantics. Rev. ed.
• Constructivism in mathematics. An introduction. Volume I
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: On the strong normalisation of intuitionistic natural deduction with permutation-conversions