Relative monads formalised

DOI10.6092/ISSN.1972-5787/4389MaRDI QIDQ5195253zbMATH OpenOpenAlexFDO

Authors Thorsten Altenkirch, James Chapman, Tarmo Uustalu

Publication date 18 September 2019

Full work available at URL https://doaj.org/article/5c63aaa6e856443f89239e99e5bb92ac

Mathematics Subject Classification ID

Monads (= standard construction, triple or triad), algebras for monads, homology and derived functors for monads (18C15) Functional programming and lambda calculus (68N18) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• Monads need not be endofunctors
• Monads need not be endofunctors
• Monads in double categories
• Dependently-typed formalisation of relation-algebraic abstractions
• scientific article; zbMATH DE number 2068087

Cited in

(7)

• C-system of a module over a \(Jf\)-relative monad
• Monads need not be endofunctors
• A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
• POPLMark reloaded: mechanizing proofs by logical relations
• Monads need not be endofunctors
• Modules over relative monads for syntax and semantics
• The formal theory of relative monads

Describes a project that uses

Uses Software

• Coq
• Haskell
• Agda

This page was built for publication: Relative monads formalised

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