Guarded computational type theory

DOI10.1145/3209108.3209153MaRDI QIDQ5145367zbMATH OpenOpenAlexFDO

Authors Jonathan Sterling, Robert Harper

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)

Full work available at URL https://arxiv.org/abs/1804.09098

zbMATH Keywords

dependent typestype theoryoperational semanticsclocksguarded recursion

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70) Functional programming and lambda calculus (68N18) Type theory (03B38)

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.

Recommendations

• Guarded dependent type theory with coinductive types
• Denotational semantics for guarded dependent type theory
• A Generalized Modality for Recursion
• The clocks are ticking: no more delays!: Reduction semantics for type theory with guarded recursion
• A model of guarded recursion with clock synchronisation

Cited in

(13)

• A metalanguage for guarded iteration
• scientific article; zbMATH DE number 1254010 (Why is no real title available?)
• Codifying guarded definitions with recursive schemes
• Denotational semantics of recursive types in synthetic guarded domain theory
• The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types
• scientific article; zbMATH DE number 7288622 (Why is no real title available?)
• Higher order functions and Brouwer's thesis
• The clocks are ticking: no more delays!: Reduction semantics for type theory with guarded recursion
• Guarded dependent type theory with coinductive types
• Denotational semantics for guarded dependent type theory
• The clocks they are adjunctions. Denotational semantics for clocked type theory
• Guarded cubical type theory
• A model of guarded recursion with clock synchronisation

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)