Denotational semantics of recursive types in synthetic guarded domain theory

DOI10.1017/S0960129518000087MaRDI QIDQ4623133zbMATH OpenOpenAlexFDO

Authors Rasmus Ejlers Møgelberg, Marco Paviotti

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) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55)

Recommendations

• Denotational semantics of recursive types in synthetic guarded domain theory
• A model of PCF in guarded type theory
• Some Domain Theory and Denotational Semantics in Coq
• Intensional type theory with guarded recursive types qua fixed points on universes
• scientific article; zbMATH DE number 1927416

Cites work

• A model of countable nondeterminism in guarded type theory
• A model of PCF in guarded type theory
• A type theory for productive coprogramming via guarded recursion
• Applicative programming with effects
• Cubical type theory: a constructive interpretation of the univalence axiom
• Denotational semantics of recursive types in synthetic guarded domain theory
• Domain-Theoretic Foundations of Functional Programming
• First steps in synthetic guarded domain theory: step-indexing in the topos of trees
• Formalized, effective domain theory in Coq
• General Recursion via Coinductive Types
• Guarded cubical type theory: path equality for guarded recursion
• Guarded dependent type theory with coinductive types
• Homotopy type theory. Univalent foundations of mathematics
• scientific article; zbMATH DE number 439891 (Why is no real title available?)
• scientific article; zbMATH DE number 19486 (Why is no real title available?)
• Impredicative concurrent abstract predicates
• Intensional type theory with guarded recursive types qua fixed points on universes
• Operational semantics using the partiality monad
• Productive coprogramming with guarded recursion
• Quotient inductive-inductive types
• Relational properties of domains
• The clocks are ticking: no more delays!: Reduction semantics for type theory with guarded recursion

Cited in

(10)

• Formalizing CCS and \(\pi\)-calculus in Guarded Cubical Agda
• The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types
• First steps in synthetic guarded domain theory: step-indexing in the topos of trees
• Denotational semantics of recursive types in synthetic guarded domain theory
• A model of PCF in guarded type theory
• Codifying guarded definitions with recursive schemes
• Greatest HITs: higher inductive types in coinductive definitions via induction under clocks
• What monads can and cannot do with a bit of extra time
• What monads can and cannot do with a few extra pages
• Scott's representation theorem and the univalent Karoubi envelope

Describes a project that uses

Uses Software

• Coq

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

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