The Blind Spot

DOI10.4171/088zbMath1238.03045OpenAlexW4245158255MaRDI QIDQ3172800

Jean-Yves Girard

Publication date: 6 October 2011

Full work available at URL: https://doi.org/10.4171/088

zbMATH Keywords

linear logicproof theoryCurry-Howard isomorphismclassical logicgeometry of interactionpolarized logic

Mathematics Subject Classification ID

Philosophical and critical aspects of logic and foundations (03A05) Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Logic in computer science (03B70) Categorical logic, topoi (03G30) Classical first-order logic (03B10) Cut-elimination and normal-form theorems (03F05) Structure of proofs (03F07) History of mathematical logic and foundations (03-03) Categorical semantics of formal languages (18C50) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15) Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Proof theory in general (including proof-theoretic semantics) (03F03) Proof theory and constructive mathematics (03Fxx)

Related Items (15)

Models of Linear Logic based on the Schwartz $\varepsilon$-product ⋮ Dialogues and Proofs; Yankov’s Contribution to Proof Theory ⋮ Category theory, logic and formal linguistics: some connections, old and new ⋮ Justification logic and type theory as formalizations of intuitionistic propositional logic ⋮ Parsing/theorem-proving for logical grammar \textit{CatLog3} ⋮ An approach to innocent strategies as graphs ⋮ Logic Discovered and Logic Imposed (A Purim Story) ⋮ Some Philosophical Aspects of Semantic Theory of Truth ⋮ Deverbal semantics and the Montagovian generative lexicon \(\Lambda \mathsf {Ty}_n\) ⋮ Interaction graphs: multiplicatives ⋮ The decidability of the intensional fragment of classical linear logic ⋮ On geometry of interaction for polarized linear logic ⋮ THE CHARACTERIZATION OF WEIHRAUCH REDUCIBILITY IN SYSTEMS CONTAINING ⋮ Transcendental syntax I: deterministic case ⋮ Comments on the Contributions

This page was built for publication: The Blind Spot