Questions tagged [step-indexing]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
2 votes
0 answers

Why Multiple Clocks in Guarded Dependent Type Theories?

The main purpose of clocks in guarded type theories (originating in Atkey & McBride ICFP 2013) is so that we can define coinductive constructions from guarded recursive definitions. Semantically ...
Max New's user avatar
  • 1,653
5 votes
2 answers

Commutativity of Clock Quantification and Disjunction/Existential Quantification in Guarded Type Theories

In Atkey & McBride ICFP 2013, they extend a simple type theory with guarded recursion indexed by clock variables $\triangleright^k$ and a clock quantification $\forall k. A$ that conveniently ...
Max New's user avatar
  • 1,653