Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type
(2017)
Conference Proceeding
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,... Read More about Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type.