A model of guarded recursion via generalised equilogical spaces

DOI10.1016/J.TCS.2018.02.012MaRDI QIDQ1704599zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

semanticsdependent type theoryequilogical spacesguarded recursion

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70)

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

Cites work

• scientific article; zbMATH DE number 2003155 (Why is no real title available?)
• scientific article; zbMATH DE number 3379785 (Why is no real title available?)
• A model of guarded recursion with clock synchronisation
• A type theory for productive coprogramming via guarded recursion
• Abstract GSOS rules and a modular treatment of recursive definitions
• Applicative programming with effects
• Behavioural differential equations: a coinductive calculus of streams, automata, and power series
• Categorical logic and type theory
• Equilogical spaces
• First steps in synthetic guarded domain theory: step-indexing in the topos of trees
• Guarded dependent type theory with coinductive types
• Impredicative concurrent abstract predicates
• Productive coprogramming with guarded recursion

Cited in

(13)

• Local local reasoning: a BI-hyperdoctrine for full ground store
• scientific article; zbMATH DE number 1696822 (Why is no real title available?)
• First steps in synthetic guarded domain theory: step-indexing in the topos of trees
• Codifying guarded definitions with recursive schemes
• 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
• Guarded cubical type theory: path equality for guarded recursion
• Guard your daggers and traces: on the equational properties of guarded (co-)recursion
• Intensional type theory with guarded recursive types qua fixed points on universes
• Guarded cubical type theory
• Computational Space Efficiency and Minimal Model Generation for Guarded Formulae
• SOME MODEL THEORY OF GUARDED NEGATION

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)