A model of guarded recursion with clock synchronisation

DOI10.1016/j.entcs.2015.12.007zbMath1351.68057OpenAlexW2221454492WikidataQ113317735 ScholiaQ113317735MaRDI QIDQ5971393

Rasmus Ejlers Møgelberg, Aleš Bizjak

Publication date: 16 December 2016

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2015.12.007

zbMATH Keywords

type theorycategorical semanticsguarded recursioncoinductive types

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Categorical semantics of formal languages (18C50) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Lewis meets Brouwer: constructive strict implication, A model of guarded recursion via generalised equilogical spaces, The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types, Denotational semantics for guarded dependent type theory, Guarded Dependent Type Theory with Coinductive Types, Guarded cubical type theory, Unnamed Item

Uses Software

• Coq

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Sheaves in geometry and logic: a first introduction to topos theory
• Categorical logic and type theory
• Copatterns
• Programming and Reasoning with Guarded Recursion for Coinductive Types
• First steps in synthetic guarded domain theory: step-indexing in the topos of trees
• A type theory for productive coprogramming via guarded recursion
• Wellfounded recursion with copatterns
• Productive coprogramming with guarded recursion
• Intensional Type Theory with Guarded Recursive Types qua Fixed Points on Universes
• Applicative programming with effects
• Univalence for inverse diagrams and homotopy canonicity