Mac Lane's comparison theorem for the Kleisli construction formalized in Coq

DOI10.1007/s11786-020-00450-8zbMath1474.68455OpenAlexW3005346743WikidataQ108482105 ScholiaQ108482105MaRDI QIDQ2209259

Cezary Kaliszyk, Burak Ekici

Publication date: 30 October 2020

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

Full work available at URL: https://doi.org/10.1007/s11786-020-00450-8

zbMATH Keywords

comparison theoremmonadsadjunctionsCoqKleisli construction

Mathematics Subject Classification ID

Adjoint functors (universal constructions, reflective subcategories, Kan extensions, etc.) (18A40) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Eilenberg-Moore and Kleisli constructions for monads (18C20) Formalization of mathematics in connection with theorem provers (68V20) Foundations, relations to logic and deductive systems (18A15)

Uses Software

• Coq
• UniMath
• Eff
• GitHub

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Programming with algebraic effects and handlers
• Notions of computation and monads
• Handling Algebraic Effects
• Experience Implementing a Performant Category-Theory Library in Coq
• A duality between exceptions and states
• Diagrammatic logic applied to a parameterisation process
• Category Theory in Coq 8.5
• An axiomatic basis for computer programming

This page was built for publication: Mac Lane's comparison theorem for the Kleisli construction formalized in Coq