The proof monad

DOI10.1016/J.JLAP.2010.03.002MaRDI QIDQ974136zbMATH OpenOpenAlexFDO

Authors Florent Kirchner, César 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

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

Recommendations

• scientific article; zbMATH DE number 3924120
• Publication:3202991
• A calculus of tactics and its operational semantics
• Monad as modality
• PVS\#: streamlined tacticals for PVS

Cites work

• scientific article; zbMATH DE number 1696760 (Why is no real title available?)
• scientific article; zbMATH DE number 4179333 (Why is no real title available?)
• scientific article; zbMATH DE number 3959364 (Why is no real title available?)
• scientific article; zbMATH DE number 4103051 (Why is no real title available?)
• scientific article; zbMATH DE number 195102 (Why is no real title available?)
• scientific article; zbMATH DE number 226803 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• scientific article; zbMATH DE number 3367095 (Why is no real title available?)
• Adjointness in Foundations
• Categorical logic and type theory
• Crafting a Proof Assistant
• Deductive systems and categories
• Edinburgh LCF. A mechanized logic of computation
• HYPERDOCTRINES, NATURAL DEDUCTION AND THE BECK CONDITION
• Locally cartesian closed categories and type theory
• Notions of computation and monads
• PVS\#: streamlined tacticals for PVS
• Rewrite strategies in the rewriting calculus
• Simple consequence relations
• Strategic computation and deduction
• The duality of computation
• Theorem proving modulo
• Tinycals: step by step tacticals

Cited in

(5)

• Just do it
• scientific article; zbMATH DE number 1692891 (Why is no real title available?)
• The Lemaître primordial atom and the monad method
• The Isbell monad
• The strategy challenge in SMT solving

Describes a project that uses

Uses Software

• ACL2
• Coq
• PVS
• LCF
• ALF

This page was built for publication: The proof monad

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