Mac Lane's comparison theorem for the Kleisli construction formalized in Coq
From MaRDI portal
Publication:2209259
Foundations, relations to logic and deductive systems (18A15) Adjoint functors (universal constructions, reflective subcategories, Kan extensions, etc.) (18A40) Eilenberg-Moore and Kleisli constructions for monads (18C20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Formalization of mathematics in connection with theorem provers (68V20)
Recommendations
- Formal proof of a machine closed theorem in Coq
- Deciding Kleene algebra terms equivalence in Coq
- Deciding Kleene algebras in \texttt{Coq}
- A Coq formalization of Lebesgue induction principle and Tonelli's theorem
- An efficient Coq tactic for deciding Kleene algebras
- On the proof theory of Coquand's calculus of constructions
- Formalized, effective domain theory in Coq
- A formal proof in Coq of Lasalle's invariance principle
- Formalizing implicative algebras in Coq
- Moessner's theorem: an exercise in coinductive reasoning in \textsc{Coq}
Cites work
- A duality between exceptions and states
- A recipe for state-and-effect triangles
- An axiomatic basis for computer programming
- Category theory in Coq 8.5
- Diagrammatic logic applied to a parameterisation process
- Experience implementing a performant category-theory library in Coq
- Handling algebraic effects
- scientific article; zbMATH DE number 2085175 (Why is no real title available?)
- scientific article; zbMATH DE number 3367095 (Why is no real title available?)
- Notions of computation and monads
- Programming with algebraic effects and handlers
This page was built for publication: Mac Lane's comparison theorem for the Kleisli construction formalized in Coq
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2209259)
