The most advanced type theory with all the above mentioned features is Clocked Type Theory (CloTT) [1]},
which introduces the notion of ticks
on a clock. Ticks are evidence that time has passed and can be used to unpack elements of type \(\triangleright ^\kappa A\)  to elements
of \(A\) . In fact, in CloTT \(\triangleright ^\kappa A\)  is generalised to a special form of dependent function type
\({\triangleright }\, (\alpha :\kappa ) .A\)  from ticks to \(A\) .
The introduction rule abstracts assumptions of the form \(\alpha : \kappa \)  from the context, and the elimination applies a
term \(t : {\triangleright }\, (\alpha :\kappa ) .A\)  to a tick \(\beta : \kappa \)  to give an element of \(A [\beta /\alpha ]\) .
Special typing rules ensure that a term is never applied twice to the same tick. The combination of ticks and clocks
in CloTT can be used for coinductive reasoning about coinductive types, by encoding the delayed substitutions
of [2]}.
