On the geometry of intuitionistic S4 proofs
DOI10.4310/HHA.2003.v5.n2.a6zbMath1022.03010MaRDI QIDQ1397803
Jean Goubault-Larrecq, Eric Goubault
Publication date: 25 September 2003
Published in: Homology, Homotopy and Applications (Search for Journal in Brave)
Full work available at URL: https://eudml.org/doc/50340
simplicial setssemanticsCurry-Howard isomorphismlambda-calculuspresheavesmonoidal comonadintuitionistic modal logic S4proofs-as-programsresolution functorsspaces of proofssubcone categories
Modal logic (including the logic of norms) (03B45) Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Resolutions; derived functors (category-theoretic aspects) (18G10) Categorical logic, topoi (03G30) Categorical semantics of formal languages (18C50) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15) Monads (= standard construction, triple or triad), algebras for monads, homology and derived functors for monads (18C15) Presheaves and sheaves, stacks, descent conditions (category-theoretic aspects) (18F20)
Related Items