Questions tagged [step-indexing]
The step-indexing tag has no usage guidance.
2
questions
2
votes
0
answers
119
views
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 ...
- 1,653
5
votes
2
answers
183
views
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 ...
- 1,653