Two guarded recursive powerdomains for applicative simulation
From MaRDI portal
Publication:6653758
DOI10.4204/EPTCS.351.13MaRDI QIDQ6653758
Rasmus Ejlers Møgelberg, Andrea Vezzosi
Publication date: 17 December 2024
Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Notions of computation and monads
- Discrete Lawvere theories and computational effects
- Relational properties of domains
- Stateful runners of effectful computations
- Step-indexed relational reasoning for countable nondeterminism
- Formalized, Effective Domain Theory in Coq
- First steps in synthetic guarded domain theory: step-indexing in the topos of trees
- Some Domain Theory and Denotational Semantics in Coq
- Countable nondeterminism and random assignment
- A note on logical relations between semantics and syntax
- Quotienting the delay monad by weak bisimilarity
- Cubical Type Theory: a constructive interpretation of the univalence axiom
- Denotational semantics of recursive types in synthetic guarded domain theory
- Runners in Action
- Operational semantics using the partiality monad
- A Model of Countable Nondeterminism in Guarded Type Theory
- Productive coprogramming with guarded recursion
- The General Universal Property of the Propositional Truncation
- General Recursion via Coinductive Types
- Homotopy Type Theory: Univalent Foundations of Mathematics
- A model of PCF in guarded type theory
This page was built for publication: Two guarded recursive powerdomains for applicative simulation
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6653758)
