Relative monads formalised
Relative monads are a generalisation of ordinary monads where the underlying functor need not be an endofunctor. In this paper, we describe a formalisation of the basic theory of relative monads in the interactive theorem prover and dependently typed programming language Agda. The formalisation comp...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Published: |
Università di Bologna
2014
|
| Online Access: | https://eprints.nottingham.ac.uk/28455/ |
| _version_ | 1848793575195672576 |
|---|---|
| author | Altenkirch, Thorsten Chapman, James Uustalu, Tarmo |
| author_facet | Altenkirch, Thorsten Chapman, James Uustalu, Tarmo |
| author_sort | Altenkirch, Thorsten |
| building | Nottingham Research Data Repository |
| collection | Online Access |
| description | Relative monads are a generalisation of ordinary monads where the underlying functor need not be an endofunctor. In this paper, we describe a formalisation of the basic theory of relative monads in the interactive theorem prover and dependently typed programming language Agda. The formalisation comprises the requisite basic category theory, the central concepts of the theory of relative monads and adjunctions, which are compared to their ordinary counterparts, and two running examples from programming theory. |
| first_indexed | 2025-11-14T19:02:28Z |
| format | Article |
| id | nottingham-28455 |
| institution | University of Nottingham Malaysia Campus |
| institution_category | Local University |
| last_indexed | 2025-11-14T19:02:28Z |
| publishDate | 2014 |
| publisher | Università di Bologna |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | nottingham-284552020-05-04T20:16:03Z https://eprints.nottingham.ac.uk/28455/ Relative monads formalised Altenkirch, Thorsten Chapman, James Uustalu, Tarmo Relative monads are a generalisation of ordinary monads where the underlying functor need not be an endofunctor. In this paper, we describe a formalisation of the basic theory of relative monads in the interactive theorem prover and dependently typed programming language Agda. The formalisation comprises the requisite basic category theory, the central concepts of the theory of relative monads and adjunctions, which are compared to their ordinary counterparts, and two running examples from programming theory. Università di Bologna 2014 Article PeerReviewed Altenkirch, Thorsten, Chapman, James and Uustalu, Tarmo (2014) Relative monads formalised. Journal of Formalized Reasoning, 7 (1). pp. 1-43. ISSN 1972-5787 http://jfr.unibo.it/article/view/4389 doi:10.6092/issn.1972-5787/4389 doi:10.6092/issn.1972-5787/4389 |
| spellingShingle | Altenkirch, Thorsten Chapman, James Uustalu, Tarmo Relative monads formalised |
| title | Relative monads formalised |
| title_full | Relative monads formalised |
| title_fullStr | Relative monads formalised |
| title_full_unstemmed | Relative monads formalised |
| title_short | Relative monads formalised |
| title_sort | relative monads formalised |
| url | https://eprints.nottingham.ac.uk/28455/ https://eprints.nottingham.ac.uk/28455/ https://eprints.nottingham.ac.uk/28455/ |