文章基本信息

标题：Relative Monads Formalised
本地全文：下载
作者：Thorsten Altenkirch ; James Chapman ; Tarmo Uustalu 等
期刊名称：Journal of Formalized Reasoning
印刷版ISSN：1972-5787
出版年度：2014
卷号：7
期号：1
页码：1-43
DOI：10.6092/issn.1972-5787/4389
语种：English
出版社：Alma Mater Studiorum - University of Bologna
摘要：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.