@inproceedings{8940cf24b8004c458204482e79d4fb22,

title = "The delay monad and restriction categories",

abstract = "We continue the study of Capretta's delay monad as a means of introducing non-termination from iteration into Martin-L{\"o}f type theory. In particular, we explain in what sense this monad provides a canonical solution. We discuss a class of monads that we call ω-complete pointed classifying monads. These are monads whose Kleisli category is an ω-complete pointed restriction category where pure maps are total. All such monads support non-termination from iteration: this is because restriction categories are a general framework for partiality; the presence of an ω-join operation on homsets equips a restriction category with a uniform iteration operator. We show that the delay monad, when quotiented by weak bisimilarity, is the initial ω-complete pointed classifying monad in our type-theoretic setting. This universal property singles it out from among other examples of such monads.",

author = "Tarmo Uustalu and Niccol{\`o} Veltri",

year = "2017",

doi = "10.1007/978-3-319-67729-3_3",

language = "English",

isbn = "978-3-319-67729-3",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "32--50",

editor = "Hung, {Dang Van} and Deepak Kapur",

booktitle = "Theoretical Aspects of Computing - ICTAC 2017: 14th International Colloquium, Hanoi, Vietnam, October 23-27, 2017, Proceedings",

address = "Germany",

note = "14th International Colloquium on Theoretical Aspects of Computing, 2017 ; Conference date: 23-10-2017 Through 27-10-2017",

}