Proofs of strong normalisation for second order classical natural deduction

DOI10.2307/2275652zbMath0941.03063OpenAlexW2132936218MaRDI 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 normalisationreducibility candidatesKolmogorov translationintuitionistic natural deductionsecond-order classical natural deduction

Mathematics Subject Classification ID

Related Items (46)

A semantical proof of the strong normalization theorem for full propositional classical natural deduction ⋮ Normalization in the simply typed -calculus ⋮ Strong normalization of the second-order symmetric \(\lambda \mu\)-calculus ⋮ The differential \(\lambda \mu\)-calculus ⋮ Programming and Proving with Classical Types ⋮ Strong normalization proofs by CPS-translations ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Mixed Inductive/Coinductive Types and Strong Normalization ⋮ Computational isomorphisms in classical logic ⋮ Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility ⋮ Adding Negation to Lambda Mu ⋮ Classical realizability and arithmetical formulæ ⋮ Structural Rules in Natural Deduction with Alternatives ⋮ Böhm theorem and Böhm trees for the \(\varLambda \mu\)-calculus ⋮ Strong normalization results by translation ⋮ Specifying Peirce's law in classical realizability ⋮ Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control ⋮ On Natural Deduction for Herbrand Constructive Logics I: Curry-Howard Correspondence for Dummett's Logic LC ⋮ Unnamed Item ⋮ A Classical Sequent Calculus with Dependent Types ⋮ A Characterisation of Lambda Definability with Sums Via ⊤ ⊤-Closure Operators ⋮ Implicative algebras: a new foundation for realizability and forcing ⋮ Domain-Freeλµ-Calculus ⋮ 2000 European Summer Meeting of the Association for Symbolic Logic. Logic Colloquium 2000 ⋮ Proof nets for classical logic ⋮ A proof-theoretic foundation of abortive continuations ⋮ Relating Computational Effects by ⊤ ⊤-Lifting ⋮ On the concurrent computational content of intermediate logics ⋮ Monadic translation of classical sequent calculus ⋮ Hypothetical logic of proofs ⋮ Strong normalization of classical natural deduction with disjunctions ⋮ Call-by-name reduction and cut-elimination in classical logic ⋮ Non-strictly positive fixed points for classical natural deduction ⋮ An estimation for the lengths of reduction sequences of the $\lambda\mu\rho\theta$-calculus ⋮ Strong normalizability of the non-deterministic catch/throw calculi ⋮ A completeness result for the simply typed \(\lambda \mu \)-calculus ⋮ A Context-based Approach to Proving Termination of Evaluation ⋮ Dual Calculus with Inductive and Coinductive Types ⋮ On the Values of Reducibility Candidates ⋮ An interpretation of \(\lambda \mu\)-calculus in \(\lambda\)-calculus. ⋮ Confluency and strong normalizability of call-by-value \(\lambda \mu\)-calculus ⋮ Relational Parametricity for Control Considered as a Computational Effect ⋮ Church-Rosser property of a simple reduction for full first-order classical natural deduction

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

This page was built for publication: Proofs of strong normalisation for second order classical natural deduction