Proofs of strong normalisation for second order classical natural deduction
From MaRDI portal
(Redirected from Publication:4382485)
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
Cites work
- A new constructive logic: classic logic
- A new deconstructive logic: linear logic
- Call-by-name, call-by-value and the \(\lambda\)-calculus
- scientific article; zbMATH DE number 42059 (Why is no real title available?)
- scientific article; zbMATH DE number 46869 (Why is no real title available?)
- scientific article; zbMATH DE number 194975 (Why is no real title available?)
- The Expressiveness of Simple and Second-Order Type Structures
Cited in
(57)- Strong normalization property for second order linear logic
- Computational isomorphisms in classical logic
- A direct proof of strong normalization for full constructive second-order 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
- Proof nets for classical logic
- On the concurrent computational content of intermediate logics
- 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
- A simple proof of second-order strong normalization with permutative conversions
- Domain-free -calculus
- 2000 European Summer Meeting of the Association for Symbolic Logic. Logic Colloquium 2000. La Sorbonne, Paris, France, July 23-31, 2000
- A context-based approach to proving termination of evaluation
- Specifying Peirce's law in classical realizability
- On natural deduction for Herbrand constructive logics. I: Curry-Howard correspondence for Dummett's logic \(\mathsf {LC}\)
- A classical sequent calculus with dependent types
- Relating Computational Effects by ⊤ ⊤-Lifting
- Classical proofs as parallel programs
- 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
- Normalization theorems for full first order classical natural deduction
- 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
- An estimation for the lengths of reduction sequences of the \(\lambda\mu\rho\theta\)-calculus
- Strong normalization proof with CPS-translation for second order classical natural deduction
- A short proof of the strong normalization of classical natural deduction with disjunction
- A NORMAL FORM THEOREM FOR SECOND-ORDER CLASSICAL LOGIC WITH AN AXIOM OF CHOICE
- scientific article; zbMATH DE number 1405618 (Why is no real title available?)
- scientific article; zbMATH DE number 7393562 (Why is no real title available?)
- Proving termination of evaluation for system F with control operators
- Hereditary substitution for the \(\lambda \Delta \)-calculus
- A note on strong normalization in classical natural deduction
- Programming and Proving with Classical Types
- Implicative algebras: a new foundation for realizability and forcing
- Relational parametricity for control considered as a computational effect
- Classical Logic with Mendler Induction
- Classical realizability and arithmetical formulæ
- Monadic translation of classical sequent calculus
- Complete call-by-value calculi of control operators. II: Strong termination
- Normalization in the simply typed -calculus
- Strong normalizability of the non-deterministic catch/throw calculi
- Adding Negation to Lambda Mu
- Structural Rules in Natural Deduction with Alternatives
- Strong normalization results by translation
- On model-theoretic strong normalization for truth-table natural deduction
- 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
- Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility
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)
