Quotienting the delay monad by weak bisimilarity

DOI10.1017/S0960129517000184MaRDI QIDQ4559601zbMATH OpenOpenAlexFDO

Authors James Chapman, Tarmo Uustalu, Niccolò Veltri

Publication date 4 December 2018

Published in Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1017/s0960129517000184

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55) Abstract data types; algebraic specification (68Q65)

Recommendations

• Quotienting the delay monad by weak bisimilarity
• The delay monad and restriction categories
• Weak bisimulations for the Giry monad
• Weak Bisimulations for the Giry Monad (Extended Abstract)
• Weak bisimulation for coalgebras over order enriched monads
• Coalgebraic Weak Bisimulation from Recursive Equations over Monads
• The weak theory of monads
• Quotient monoids and concurrent behaviours
• scientific article; zbMATH DE number 3841844
• The Vietoris monad and weak distributive laws

Cites work

• Categorical semantics for arrows
• Constructivism in mathematics. An introduction. Volume II
• Containers: Constructing strictly positive types
• Dependently typed programming in Agda
• Extensional constructs in intensional type theory
• General Recursion via Coinductive Types
• Generalising monads to arrows
• Generalizations of Hedberg's theorem
• scientific article; zbMATH DE number 19486 (Why is no real title available?)
• scientific article; zbMATH DE number 2003152 (Why is no real title available?)
• Metric spaces in synthetic topology
• Notions of computation and monads
• Partial map classifiers and partial cartesian closed categories
• Partiality, Revisited
• Synthetic topology: of data types and classical spaces
• Timed Sets, Functional Complexity, and Computability
• Unguarded recursion on coinductive resumptions
• When is a container a comonad?

Cited in

(16)

• The delay monad and restriction categories
• The construction of set-truncated higher inductive types
• Formalizing CCS and \(\pi\)-calculus in Guarded Cubical Agda
• Quotienting the delay monad by weak bisimilarity
• Constructing higher inductive types as groupoid quotients
• scientific article; zbMATH DE number 7362470 (Why is no real title available?)
• The Scott model of PCF in univalent type theory
• Streams of approximations, equivalence of recursive effectful programs
• A type system with subtyping for WebAssembly's stack polymorphism
• Greatest HITs: higher inductive types in coinductive definitions via induction under clocks
• Two guarded recursive powerdomains for applicative simulation
• Inductive and coinductive predicate liftings for effectful programs
• Representing guardedness in call-by-value and guarded parametrized monads
• What monads can and cannot do with a bit of extra time
• What monads can and cannot do with a few extra pages
• Uniform Elgot iteration in foundations

Describes a project that uses

Uses Software

• Agda
• HoTT

This page was built for publication: Quotienting the delay monad by weak bisimilarity

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