Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi

DOI10.1016/0304-3975(93)90011-HzbMath0772.03026OpenAlexW2134699386MaRDI QIDQ1208732

Jean H. Gallier

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

zbMATH Keywords

linear logicnatural deductionintuitionistic logicproof systemssequent calculiclassical logicconstructive logicsGödel's translationstyped \(\lambda\)-calculi

Mathematics Subject Classification ID

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

Pattern matching as cut elimination, Strong normalization and typability with intersection types, New Curry-Howard terms for full linear logic, UNDER LOCK AND KEY: A PROOF SYSTEM FOR A MULTIMODAL LOGIC, Extracting \(\mathsf{BB'IW}\) inhabitants of simple types from proofs in the sequent calculus \(LT_\to^t\) for implicational ticket entailment, Cut Elimination in a Class of Sequent Calculi for Pure Type Systems, On the form of witness terms, On structuring proof search for first order linear logic, Unnamed Item, Representing scope in intuitionistic deductions, Revisiting Zucker’s Work on the Correspondence Between Cut-Elimination and Normalisation, Structural cut elimination. I: Intuitionistic and classical logic, Conservation and uniform normalization in lambda calculi with erasing reductions

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