Denotational semantics of recursive types in synthetic guarded domain theory

DOI10.1017/S0960129518000087zbMath1411.68030OpenAlexW2803229276MaRDI QIDQ4623133

Marco Paviotti, Rasmus Ejlers Møgelberg

Publication date: 19 February 2019

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

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

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (1)

Formalizing CCS and \(\pi\)-calculus in Guarded Cubical Agda

Uses Software

• Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Quotient inductive-inductive types
• Relational properties of domains
• Guarded Dependent Type Theory with Coinductive Types
• Formalized, Effective Domain Theory in Coq
• First steps in synthetic guarded domain theory: step-indexing in the topos of trees
• Domain-Theoretic Foundations of Functional Programming
• Cubical Type Theory: a constructive interpretation of the univalence axiom
• A type theory for productive coprogramming via guarded recursion
• Denotational semantics of recursive types in synthetic guarded domain theory
• Operational semantics using the partiality monad
• A Model of Countable Nondeterminism in Guarded Type Theory
• Productive coprogramming with guarded recursion
• Intensional Type Theory with Guarded Recursive Types qua Fixed Points on Universes
• Guarded Cubical Type Theory: Path Equality for Guarded Recursion
• General Recursion via Coinductive Types
• Impredicative Concurrent Abstract Predicates
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Applicative programming with effects
• A model of PCF in guarded type theory

This page was built for publication: Denotational semantics of recursive types in synthetic guarded domain theory