Partiality, revisited: the partiality monad as a quotient inductive-inductive type

Capretta's delay monad can be used to model partial computations, but it has the "wrong" notion of built-in equality, strong bisimilarity. An alternative is to quotient the delay monad by the "right" notion of equality, weak bisimilarity. However, recent work by Chapman et a...

Full description

Bibliographic Details
Main Authors: Altenkirch, Thorsten, Danielsson, Nils Anders, Kraus, Nicolai
Format: Article
Published: Springer Verlag 2017
Subjects:
Online Access:https://eprints.nottingham.ac.uk/38095/