The proof monad

DOI10.1016/j.jlap.2010.03.002zbMath1208.68144OpenAlexW2074233181MaRDI QIDQ974136

Florent Kirchner, César A. Muñoz

Publication date: 27 May 2010

Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlap.2010.03.002

zbMATH Keywords

category theorydeductive strategiesmonadic structuresproof languages

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Monads (= standard construction, triple or triad), algebras for monads, homology and derived functors for monads (18C15)

Related Items (1)

The Strategy Challenge in SMT Solving

Uses Software

• ACL2
• Coq
• PVS
• LCF
• ALF

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Notions of computation and monads
• Simple consequence relations
• Categorical logic and type theory
• Theorem proving modulo
• Edinburgh LCF. A mechanized logic of computation
• PVS#: Streamlined Tacticals for PVS
• Tinycals: Step by Step Tacticals
• The duality of computation
• Locally cartesian closed categories and type theory
• Crafting a Proof Assistant
• HYPERDOCTRINES, NATURAL DEDUCTION AND THE BECK CONDITION
• Adjointness in Foundations
• Deductive systems and categories

This page was built for publication: The proof monad