English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Zendy Plus

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Zendy Tools

Zendy Open

Guarded recursion is a powerful modal approach to recursion that can be seenas an abstract form of step-indexing. It is currently used extensively inseparation logic to model programming languages with advanced features bysolving domain equations also with negative occurrences. In its multi-clockedversion, guarded recursion can also be used to program with and reason aboutcoinductive types, encoding the productivity condition required for recursivedefinitions in types. This paper presents the first type theory combiningmulti-clocked guarded recursion with the features of Cubical Type Theory, aswell as a denotational semantics. Using the combination of Higher InductiveTypes (HITs) and guarded recursion allows for simple programming and reasoningabout coinductive types that are traditionally hard to represent in typetheory, such as the type of finitely branching labelled transition systems. Forexample, our results imply that bisimilarity for these imply path equality, andso proofs can be transported along bisimilarity proofs. Among our technicalcontributions is a new principle of induction under clocks. This allowsuniversal quantification over clocks to commute with HITs up to equivalence oftypes, and is crucial for the encoding of coinductive types. Such commutativityrequirements have been formulated for inductive types as axioms in previoustype theories with multi-clocked guarded recursion, but our present formulationas an induction principle allows for the formulation of general computationrules.

Greatest HITs: Higher inductive types in coinductive definitions via induction under clocks