Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi
DOI10.1016/0304-3975(93)90011-HzbMath0772.03026OpenAlexW2134699386MaRDI QIDQ1208732
Publication date: 16 May 1993
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0304-3975(93)90011-h
linear logicnatural deductionintuitionistic logicproof systemssequent calculiclassical logicconstructive logicsGödel's translationstyped \(\lambda\)-calculi
Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations (03-01) Logic in computer science (03B70) Proof theory in general (including proof-theoretic semantics) (03F03) Subsystems of classical logic (including intuitionistic logic) (03B20) Combinatory logic and lambda calculus (03B40)
Related Items
Cites Work
- Linear logic
- Computational interpretations of linear logic
- The lambda calculus, its syntax and semantics
- Constructivism in mathematics. An introduction. Volume II
- Linearizing intuitionistic implication
- Combinators, \(\lambda\)-terms and proof theory
- A new constructive logic: classic logic
- On an interpretation of second order quantification in first order intuitionistic propositional logic
- Contraction-free sequent calculi for intuitionistic logic
- The correspondence between cut-elimination and normalization
- Intensional interpretations of functionals of finite type I
- A new algorithm for derivability in the constructive propositional calculus
- Logic and structure
- Proof theory
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item