The delay monad and restriction categories

Tarmo Uustalu, Niccolò Veltri

Publikation: Konference artikel i Proceeding eller bog/rapport kapitelKonferencebidrag i proceedingsForskningpeer review

Abstrakt

We continue the study of Capretta's delay monad as a means of introducing non-termination from iteration into Martin-Lö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.
OriginalsprogEngelsk
TitelTheoretical Aspects of Computing - ICTAC 2017: 14th International Colloquium, Hanoi, Vietnam, October 23-27, 2017, Proceedings
RedaktørerDang Van Hung, Deepak Kapur
Antal sider19
UdgivelsesstedCham
ForlagSpringer
Publikationsdato2017
Sider32-50
ISBN (Trykt)978-3-319-67729-3
DOI
StatusUdgivet - 2017
Udgivet eksterntJa
Begivenhed14th International Colloquium on Theoretical Aspects of Computing, 2017 -
Varighed: 23 okt. 201727 okt. 2017

Konference

Konference14th International Colloquium on Theoretical Aspects of Computing, 2017
Periode23/10/201727/10/2017
NavnLecture Notes in Computer Science
Vol/bind10580
ISSN0302-9743

Fingeraftryk

Dyk ned i forskningsemnerne om 'The delay monad and restriction categories'. Sammen danner de et unikt fingeraftryk.

Citationsformater