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/

Global: Zendy Plus annual

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

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Clocked Cubical Type Theory is a new type theory combining the power ofguarded recursion with univalence and higher inductive types (HITs). This typetheory can be used as a metalanguage for synthetic guarded domain theory inwhich one can solve guarded recursive type equations, also with negativevariable occurrences, and use these to construct models for reasoning aboutprogramming languages. Combining this with HITs allows for the use of typeconstructors familiar from set-theory based approaches to semantics, such asquotients and finite powersets in these models.  In this paper we show how to reason about the combination of finitenon-determinism and recursion in this type theory. Unlike traditional domaintheory which takes an ordering of programs as primitive, synthetic guardeddomain theory takes the notion of computation step as primitive in the form ofa modal operator. We use this extra intensional information to define twoguarded recursive (finite) powerdomain constructions differing in the waynon-determinism interacts with the computation steps. As an example applicationof these we show how to prove applicative similarity a congruence in the casesof may- and must-convergence for the untyped lambda calculus with finitenon-determinism. Such results are usually proved using operational reasoningand Howe's method. Here we use an adaptation of a denotational method developedby Pitts in the context of domain theory.

Two Guarded Recursive Powerdomains for Applicative Simulation