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 e...

Full description

Bibliographic Details
Main Authors: Altenkirch, Thorsten, Danielson, Nils Anders, Kraus, Nicolai
Format: Conference or Workshop Item
Published: 2016
Online Access:https://eprints.nottingham.ac.uk/41533/