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

zbMATH Keywords

simplicial setssemanticsCurry-Howard isomorphismlambda-calculuspresheavesmonoidal comonadintuitionistic modal logic S4proofs-as-programsresolution functorsspaces of proofssubcone categories

Mathematics Subject Classification ID

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

Logical relations for monadic types, Modes of adjointness, A convenient category of locally preordered spaces