On Natural Deduction for Herbrand Constructive Logics I: Curry-Howard Correspondence for Dummett's Logic LC
From MaRDI portal
Publication:2974784
DOI10.2168/LMCS-12(3:13)2016zbMath1445.03005arXiv1609.03190OpenAlexW2950132283MaRDI QIDQ2974784
Publication date: 11 April 2017
Published in: Logical Methods in Computer Science (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1609.03190
Cut-elimination and normal-form theorems (03F05) Subsystems of classical logic (including intuitionistic logic) (03B20) Combinatory logic and lambda calculus (03B40)
Related Items (2)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- On natural deduction in classical first-order logic: Curry-Howard correspondence, strong normalization and Herbrand's theorem
- Classical logic, storage operators and second-order lambda-calculus
- Hypersequents, logical consequence and intermediate logics for concurrency
- A cut-free calculus for second-order Gödel logic
- Untersuchungen über das logische Schliessen. I
- A Lambda Calculus for Gödel–Dummett Logic Capturing Waitfreedom
- Gentzen's Proof of Normalization for Natural Deduction
- A Cut‐Free Calculus For Dummett's LC Quantified
- Proofs of strong normalisation for second order classical natural deduction
- Interactive Realizability for Classical Peano Arithmetic with Skolem Axioms
- Hypersequent Calculi for Godel Logics -- a Survey
- Separating intermediate predicate logics of well-founded and dually well-founded structures by monadic sentences
- Non-determinism, Non-termination and the Strong Normalization of System T
- On the interpretation of intuitionistic number theory
This page was built for publication: On Natural Deduction for Herbrand Constructive Logics I: Curry-Howard Correspondence for Dummett's Logic LC
