Partiality and Container Monads

DOI10.1007/978-3-319-71237-6_20MaRDI QIDQ5056003zbMATH OpenOpenAlexFDO

Authors Tarmo Uustalu, Niccolò Veltri

Publication date 9 December 2022

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-71237-6_20

Mathematics Subject Classification ID

Type theory (03B38) Logic in computer science (03B70) Monads (= standard construction, triple or triad), algebras for monads, homology and derived functors for monads (18C15)

Recommendations

• Partiality, Revisited
• Container combinatorics: monads and lax monoidal functors
• The delay monad and restriction categories
• scientific article; zbMATH DE number 1497816
• An equational notion of lifting monad

Cites work

• An equational notion of lifting monad
• Categories of partial maps
• Container combinatorics: monads and lax monoidal functors
• Containers: Constructing strictly positive types
• Dependently typed programming in Agda
• General Recursion via Coinductive Types
• Homotopy type theory. Univalent foundations of mathematics
• scientific article; zbMATH DE number 3574077 (Why is no real title available?)
• Notions of computation and monads
• Partial elements and recursion via dominances in univalent type theory
• Partiality and recursion in interactive theorem provers -- an overview
• Partiality, Revisited
• Quotienting the delay monad by weak bisimilarity
• Restriction categories II: Partial map classification
• Restriction categories III: colimits, partial limits and extensivity
• Restriction categories. I: Categories of partial maps
• Stack semantics of type theory
• Synthetic topology: of data types and classical spaces
• The delay monad and restriction categories
• When is a container a comonad?

Cited in

(7)

• An equational notion of lifting monad
• The delay monad and restriction categories
• Quotienting the delay monad by weak bisimilarity
• Update monads: cointerpreting directed containers
• Partiality, Revisited
• Operational semantics using the partiality monad
• Uniform Elgot iteration in foundations

Describes a project that uses

Uses Software

• Agda

This page was built for publication: Partiality and Container Monads

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5056003)