Proofs of strong normalisation for second order classical natural deduction

DOI10.2307/2275652zbMATH Open0941.03063OpenAlexW2132936218MaRDI QIDQ4382485FDOQ4382485

Authors: 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

Recommendations

• Strong normalization proof with CPS-translation for second order classical natural deduction
• A note on strong normalization in classical natural deduction
• A direct proof of strong normalization for full constructive second-order logic
• A semantical proof of the strong normalization theorem for full propositional classical natural deduction
• Normalization theorems for full first order classical natural deduction
• Strong normalization of a symmetric lambda calculus for second-order classical logic
• Strong normalization of classical natural deduction with disjunctions
• On natural deduction in classical first-order logic: Curry-Howard correspondence, strong normalization and Herbrand's theorem
• scientific article; zbMATH DE number 1722654
• A strong normalization result for classical logic

zbMATH Keywords

strong normalisationreducibility candidatesKolmogorov translationintuitionistic natural deductionsecond-order classical natural deduction

Mathematics Subject Classification ID

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

Cites Work

• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Title not available (Why is that?)
• A new constructive logic: classic logic
• Title not available (Why is that?)
• The Expressiveness of Simple and Second-Order Type Structures
• A new deconstructive logic: linear logic
• Title not available (Why is that?)

Cited In (55)

• Adding Negation to Lambda Mu
• Structural Rules in Natural Deduction with Alternatives
• An interpretation of \(\lambda \mu\)-calculus in \(\lambda\)-calculus.
• Confluency and strong normalizability of call-by-value \(\lambda \mu\)-calculus
• Programming and Proving with Classical Types
• Title not available (Why is that?)
• 2000 European Summer Meeting of the Association for Symbolic Logic. Logic Colloquium 2000. La Sorbonne, Paris, France, July 23-31, 2000
• On the concurrent computational content of intermediate logics
• Strong normalization of classical natural deduction with disjunctions
• A simple proof of second-order strong normalization with permutative conversions
• Hereditary substitution for the \(\lambda \Delta \)-calculus
• Monadic translation of classical sequent calculus
• Strong normalization proofs by CPS-translations
• Classical realizability and arithmetical formulæ
• Church-Rosser property of a simple reduction for full first-order classical natural deduction
• Strong normalization property for second order linear logic
• An estimation for the lengths of reduction sequences of the \(\lambda\mu\rho\theta\)-calculus
• On natural deduction for Herbrand constructive logics. I: Curry-Howard correspondence for Dummett's logic \(\mathsf {LC}\)
• A Characterisation of Lambda Definability with Sums Via ⊤ ⊤-Closure Operators
• Mixed Inductive/Coinductive Types and Strong Normalization
• Relational parametricity for control considered as a computational effect
• Call-by-name reduction and cut-elimination in classical logic
• Computational isomorphisms in classical logic
• Hypothetical logic of proofs
• A classical sequent calculus with dependent types
• Relating Computational Effects by ⊤ ⊤-Lifting
• Complete call-by-value calculi of control operators. II: Strong termination
• A note on strong normalization in classical natural deduction
• Böhm theorem and Böhm trees for the \(\varLambda \mu\)-calculus
• Classical Logic with Mendler Induction
• A short proof of the strong normalization of classical natural deduction with disjunction
• Proving termination of evaluation for system F with control operators
• The differential \(\lambda \mu\)-calculus
• A context-based approach to proving termination of evaluation
• A proof-theoretic foundation of abortive continuations
• Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility
• Domain-free \(\lambda\mu\)-calculus
• Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control
• Specifying Peirce's law in classical realizability
• Normalization in the simply typed -calculus
• Strong normalization results by translation
• Title not available (Why is that?)
• Title not available (Why is that?)
• A NORMAL FORM THEOREM FOR SECOND-ORDER CLASSICAL LOGIC WITH AN AXIOM OF CHOICE
• Implicative algebras: a new foundation for realizability and forcing
• A semantical proof of the strong normalization theorem for full propositional classical natural deduction
• Dual Calculus with Inductive and Coinductive Types
• On the Values of Reducibility Candidates
• Strong normalization of the second-order symmetric \(\lambda \mu\)-calculus
• A direct proof of strong normalization for full constructive second-order logic
• Non-strictly positive fixed points for classical natural deduction
• Strong normalizability of the non-deterministic catch/throw calculi
• Strong normalization proof with CPS-translation for second order classical natural deduction
• Proof nets for classical logic
• A completeness result for the simply typed \(\lambda \mu \)-calculus

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4382485)