Clocks as First Class Abstract Types

摘要

Clocks in synchronous data-flow languages are the natural way to define several time scales in reactive systems. They play a fundamental role during the specification of the system and are largely used in the compilation process to generate efficient sequential code. Based on the formulation of clocks as dependent types, the paper presents a simpler clock calculus reminiscent to ML type systems with first order abstract types a la Laufer & Odersky. Not only this system provides clock inference, it shares efficient implementations of ML type systems and appears to be expressive enough for many real applications.