A model of guarded recursion via generalised equilogical spaces

DOI10.1016/J.TCS.2018.02.012zbMath1388.68023OpenAlexW2790472081MaRDI QIDQ1704599

Lars Birkedal, Aleš Bizjak

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

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

Related Items (1)

Local local reasoning: a BI-hyperdoctrine for full ground store

Cites Work

• Unnamed Item
• Unnamed Item
• Categorical logic and type theory
• Equilogical spaces
• Behavioural differential equations: a coinductive calculus of streams, automata, and power series
• Guarded Dependent Type Theory with Coinductive Types
• Abstract GSOS Rules and a Modular Treatment of Recursive Definitions
• First steps in synthetic guarded domain theory: step-indexing in the topos of trees
• A type theory for productive coprogramming via guarded recursion
• Productive coprogramming with guarded recursion
• Impredicative Concurrent Abstract Predicates
• Applicative programming with effects
• A model of guarded recursion with clock synchronisation

This page was built for publication: A model of guarded recursion via generalised equilogical spaces