Proofs of strong normalisation for second order classical natural deduction

DOI10.2307/2275652zbMath0941.03063MaRDI QIDQ4382485

Michel Parigot

Publication date: 29 April 1998

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

Full work available at URL: https://doi.org/10.2307/2275652

zbMATH Keywords

strong normalisation; reducibility candidates; Kolmogorov translation; intuitionistic natural deduction; second-order classical natural deduction

Mathematics Subject Classification ID

03F05: Cut-elimination and normal-form theorems

Related Items

Relational Parametricity for Control Considered as a Computational Effect, Monadic translation of classical sequent calculus, Strong normalizability of the non-deterministic catch/throw calculi, Böhm theorem and Böhm trees for the \(\varLambda \mu\)-calculus, Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control, Strong normalization results by translation, A completeness result for the simply typed \(\lambda \mu \)-calculus, A semantical proof of the strong normalization theorem for full propositional classical natural deduction, Strong normalization proofs by CPS-translations, Computational isomorphisms in classical logic, Non-strictly positive fixed points for classical natural deduction, An interpretation of \(\lambda \mu\)-calculus in \(\lambda\)-calculus., Confluency and strong normalizability of call-by-value \(\lambda \mu\)-calculus, Church-Rosser property of a simple reduction for full first-order classical natural deduction, Strong normalization of the second-order symmetric \(\lambda \mu\)-calculus, Hypothetical logic of proofs, The differential \(\lambda \mu\)-calculus, A proof-theoretic foundation of abortive continuations, Strong normalization of classical natural deduction with disjunctions, Call-by-name reduction and cut-elimination in classical logic, Domain-Freeλµ-Calculus, 2000 European Summer Meeting of the Association for Symbolic Logic. Logic Colloquium 2000, Relating Computational Effects by ⊤ ⊤-Lifting, Mixed Inductive/Coinductive Types and Strong Normalization, A Characterisation of Lambda Definability with Sums Via ⊤ ⊤-Closure Operators, Dual Calculus with Inductive and Coinductive Types, On the Values of Reducibility Candidates

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• The Expressiveness of Simple and Second-Order Type Structures
• A new constructive logic: classic logic
• A new deconstructive logic: linear logic