Two guarded recursive powerdomains for applicative simulation
From MaRDI portal
Cites work
- A model of countable nondeterminism in guarded type theory
- A model of PCF in guarded type theory
- A note on logical relations between semantics and syntax
- Countable nondeterminism and random assignment
- Cubical type theory: a constructive interpretation of the univalence axiom
- Denotational semantics of recursive types in synthetic guarded domain theory
- Discrete Lawvere theories and computational effects
- Effectful applicative bisimilarity: monads, relators, and Howe's method
- 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
- Homotopy type theory. Univalent foundations of mathematics
- scientific article; zbMATH DE number 4180818 (Why is no real title available?)
- scientific article; zbMATH DE number 794258 (Why is no real title available?)
- scientific article; zbMATH DE number 7288622 (Why is no real title available?)
- Notions of computation and monads
- Operational semantics using the partiality monad
- Productive coprogramming with guarded recursion
- Quotienting the delay monad by weak bisimilarity
- Relational properties of domains
- Runners in Action
- Some Domain Theory and Denotational Semantics in Coq
- Stateful runners of effectful computations
- Step-indexed relational reasoning for countable nondeterminism
- The general universal property of the propositional truncation
Cited in
(2)
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)
