Monad as modality

DOI10.1016/S0304-3975(96)00169-7zbMath0895.03011MaRDI QIDQ1392142

Satoshi Kobayashi

Publication date: 23 July 1998

Published in: Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

equational logicmodal logicsCurry-Howard correspondenceprogram semanticsgeneralization of string monadsmethod to extract a monad-based imperative functional program from a proof

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Categorical logic, topoi (03G30) Monads (= standard construction, triple or triad), algebras for monads, homology and derived functors for monads (18C15)

Related Items (14)

A dual-context sequent calculus for the constructive modal logic S4 ⋮ Towards a Common Categorical Semantics for Linear-Time Temporal Logic and Functional Reactive Programming ⋮ Abstract categorical semantics for resourceful functional reactive programming ⋮ Lewis meets Brouwer: constructive strict implication ⋮ Reduction rules for intuitionistic \(\lambda\rho\)-calculus ⋮ Dual and axiomatic systems for constructive S4, a formally verified equivalence ⋮ Domain-Freeλµ-Calculus ⋮ Fibrational modal type theory ⋮ Connectionist computations of intuitionistic reasoning ⋮ A general method for proving decidability of intuitionistic modal logics ⋮ Game Semantics for Access Control ⋮ Axiomatic and dual systems for constructive necessity, a formally verified equivalence ⋮ Cut-free Gentzen calculus for multimodal CK ⋮ Constructive linear-time temporal logic: proof systems and Kripke semantics

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Constructive modal logics. I
• Notions of computation and monads
• Constructivism in mathematics. An introduction. Volume II
• On an intuitionistic modal logic
• Strong functors and monoidal monads
• Comprehending monads
• Programs with continuations and linear logic

This page was built for publication: Monad as modality