Overture

The goal of the Overture project is to produce a language for embedded real-time systems that allows programmers to use dependent clocks to compose communicating tasks. The current implementation of Overture is simply a modified Prelude compiler that generates ATS code for the purpose of typechecking. The clock calculus that the Prelude type checker utilizes for proving all communication done in a program is synchronized can be readily expressed using the restricted form of dependent types found in ATS.

To take Prelude a step further, we can use the ATS compiler’s meta-programming features to construct a synchronous language that shares ATS’ syntax and that supports dependent clocks for verifying synchronized communication. That is, the clock associated with a given flow may be defined in terms of other clocks.