Guarded Computational Type Theory
From MaRDI portal
Publication:5145367
DOI10.1145/3209108.3209153zbMATH Open1453.03027arXiv1804.09098OpenAlexW2964121680MaRDI QIDQ5145367FDOQ5145367
Robert Harper, Jonathan Sterling
Publication date: 20 January 2021
Published in: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)
Abstract: Nakano's later modality can be used to specify and define recursive functions which are causal or synchronous; in concert with a notion of clock variable, it is possible to also capture the broader class of productive (co)programs. Until now, it has been difficult to combine these constructs with dependent types in a way that preserves the operational meaning of type theory and admits a hierarchy of universes. We present an operational account of guarded dependent type theory with clocks called Guarded Computational Type Theory, featuring a novel clock intersection connective that enjoys the clock irrelevance principle, as well as a predicative hierarchy of universes which does not require any indexing in clock contexts. Guarded Computational Type Theory is simultaneously a programming language with a rich specification logic, as well as a computational metalanguage that can be used to develop semantics of other languages and logics.
Full work available at URL: https://arxiv.org/abs/1804.09098
Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70) Functional programming and lambda calculus (68N18) Type theory (03B38)
Cited In (8)
- The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types
- Title not available (Why is that?)
- Higher order functions and Brouwer’s thesis
- A metalanguage for guarded iteration
- Title not available (Why is that?)
- Denotational semantics for guarded dependent type theory
- Denotational semantics of recursive types in synthetic guarded domain theory
- Codifying guarded definitions with recursive schemes
This page was built for publication: Guarded Computational Type Theory
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5145367)
