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

In type theory, coinductive types are used to represent processes, and arethus crucial for the formal verification of non-terminating reactive programsin proof assistants based on type theory, such as Coq and Agda. Currently,programming and reasoning about coinductive types is difficult for two reasons:The need for recursive definitions to be productive, and the lack ofcoincidence of the built-in identity types and the important notion ofbisimilarity.  Guarded recursion in the sense of Nakano has recently been suggested as apossible approach to dealing with the problem of productivity, allowing this tobe encoded in types. Indeed, coinductive types can be encoded using acombination of guarded recursion and universal quantification over clocks. Thispaper studies the notion of bisimilarity for guarded recursive types in TickedCubical Type Theory, an extension of Cubical Type Theory with guardedrecursion. We prove that, for any functor, an abstract, category theoreticnotion of bisimilarity for the final guarded coalgebra is equivalent (in thesense of homotopy type theory) to path equality (the primitive notion ofequality in cubical type theory). As a worked example we study a guarded notionof labelled transition systems, and show that, as a special case of the generaltheorem, path equality coincides with an adaptation of the usual notion ofbisimulation for processes. In particular, this implies that guarded recursioncan be used to give simple equational reasoning proofs of bisimilarity. Thiswork should be seen as a step towards obtaining bisimilarity as path equalityfor coinductive types using the encodings mentioned above.

Bisimulation as path type for guarded recursive types