A model of guarded recursion via generalised equilogical spaces
From MaRDI portal
Publication:1704599
DOI10.1016/J.TCS.2018.02.012zbMATH Open1388.68023OpenAlexW2790472081MaRDI QIDQ1704599FDOQ1704599
Authors: Aleš Bizjak, Lars Birkedal
Publication date: 12 March 2018
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.tcs.2018.02.012
Recommendations
- Guard your daggers and traces: on the equational properties of guarded (co-)recursion
- Guards, bounds, and generalized semantics
- A model of PCF in guarded type theory
- Codifying guarded definitions with recursive schemes
- Computational Space Efficiency and Minimal Model Generation for Guarded Formulae
- A note on guarded theories
- Programming and reasoning with guarded recursion for coinductive types
- SOME MODEL THEORY OF GUARDED NEGATION
- A model of countable nondeterminism in guarded type theory
- A model of guarded recursion with clock synchronisation
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70)
Cites Work
- Categorical logic and type theory
- Impredicative concurrent abstract predicates
- Title not available (Why is that?)
- Equilogical spaces
- Behavioural differential equations: a coinductive calculus of streams, automata, and power series
- Abstract GSOS rules and a modular treatment of recursive definitions
- Applicative programming with effects
- First steps in synthetic guarded domain theory: step-indexing in the topos of trees
- Guarded dependent type theory with coinductive types
- A type theory for productive coprogramming via guarded recursion
- Productive coprogramming with guarded recursion
- A model of guarded recursion with clock synchronisation
- Title not available (Why is that?)
Cited In (13)
- First steps in synthetic guarded domain theory: step-indexing in the topos of trees
- Computational Space Efficiency and Minimal Model Generation for Guarded Formulae
- Guarded cubical type theory
- SOME MODEL THEORY OF GUARDED NEGATION
- Title not available (Why is that?)
- A model of PCF in guarded type theory
- A model of countable nondeterminism in guarded type theory
- Programming and reasoning with guarded recursion for coinductive types
- Intensional type theory with guarded recursive types qua fixed points on universes
- Guarded cubical type theory: path equality for guarded recursion
- Codifying guarded definitions with recursive schemes
- Guard your daggers and traces: on the equational properties of guarded (co-)recursion
- Local local reasoning: a BI-hyperdoctrine for full ground store
This page was built for publication: A model of guarded recursion via generalised equilogical spaces
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1704599)