Monad as modality

DOI10.1016/S0304-3975(96)00169-7MaRDI QIDQ1392142zbMATH OpenFDO

Authors Satoshi Kobayashi

Publication date 23 July 1998

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

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)

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

Cites work

• scientific article; zbMATH DE number 431759 (Why is no real title available?)
• scientific article; zbMATH DE number 4179333 (Why is no real title available?)
• scientific article; zbMATH DE number 4033710 (Why is no real title available?)
• scientific article; zbMATH DE number 3367095 (Why is no real title available?)
• Comprehending monads
• Constructive modal logics. I
• Constructivism in mathematics. An introduction. Volume II
• Notions of computation and monads
• On an intuitionistic modal logic
• Programs with continuations and linear logic
• Strong functors and monoidal monads

Cited in

(21)

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