Quotienting the delay monad by weak bisimilarity

DOI10.1017/S0960129517000184zbMath1407.68306OpenAlexW2767001837MaRDI QIDQ4559601

Niccolò Veltri, Tarmo Uustalu, James T. E. Chapman

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)

Related Items

The construction of set-truncated higher inductive types, The Scott model of PCF in univalent type theory, Unnamed Item, Streams of approximations, equivalence of recursive effectful programs, A type system with subtyping for WebAssembly's stack polymorphism, Formalizing CCS and \(\pi\)-calculus in Guarded Cubical Agda

Uses Software

• Agda
• HoTT

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Metric spaces in synthetic topology
• Notions of computation and monads
• Constructivism in mathematics. An introduction. Volume II
• Partial map classifiers and partial cartesian closed categories
• Generalising monads to arrows
• Containers: Constructing strictly positive types
• When is a container a comonad?
• Partiality, Revisited
• Timed Sets, Functional Complexity, and Computability
• Categorical semantics for arrows
• Dependently Typed Programming in Agda
• Extensional Constructs in Intensional Type Theory
• Generalizations of Hedberg’s Theorem
• General Recursion via Coinductive Types
• Unguarded recursion on coinductive resumptions