Monad as modality

DOI10.1016/S0304-3975(96)00169-7zbMATH Open0895.03011MaRDI QIDQ1392142FDOQ1392142

Authors: Satoshi Kobayashi 

Publication date: 23 July 1998

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

Recommendations

• Computational types from a logical perspective
• A MONADIC APPROACH TO THE MODAL THEORY
• Notions of monad strength
• Monad-independent dynamic logic in HasCasl.
• scientific article; zbMATH DE number 3924120

zbMATH Keywords

Curry-Howard correspondencemodal logicsprogram semanticsequational logicgeneralization 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) Categorical logic, topoi (03G30) Monads (= standard construction, triple or triad), algebras for monads, homology and derived functors for monads (18C15) Semantics in the theory of computing (68Q55)

Cites Work

• On an intuitionistic modal logic
• Title not available (Why is that?)
• Notions of computation and monads
• Title not available (Why is that?)
• Title not available (Why is that?)
• Strong functors and monoidal monads
• Comprehending monads
• Constructivism in mathematics. An introduction. Volume II
• Constructive modal logics. I
• Title not available (Why is that?)
• Programs with continuations and linear logic

Cited In (21)

• Dual and axiomatic systems for constructive S4, a formally verified equivalence
• Axiomatic and dual systems for constructive necessity, a formally verified equivalence
• A dual-context sequent calculus for the constructive modal logic S4
• The proof monad
• Fibrational modal type theory
• Connectionist computations of intuitionistic reasoning
• Notions of monad strength
• A general method for proving decidability of intuitionistic modal logics
• The Isbell monad
• Reduction rules for intuitionistic \(\lambda\rho\)-calculus
• Game semantics for access control
• Domain-free \(\lambda\mu\)-calculus
• Abstract categorical semantics for resourceful functional reactive programming
• Title not available (Why is that?)
• Constructive linear-time temporal logic: proof systems and Kripke semantics
• Cut-free Gentzen calculus for multimodal CK
• Title not available (Why is that?)
• Monad-independent dynamic logic in HasCasl.
• Lewis meets Brouwer: constructive strict implication
• The Lemaître primordial atom and the monad method
• Towards a common categorical semantics for linear-time temporal logic and functional reactive programming

This page was built for publication: Monad as modality

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1392142)