up: Publications

Clock type soundness in synchronous languages

Martin Strecker


Synchronous languages are based on the hypothesis that computations of a program are carried out at specific instants, as determined by the clocks of the signals processed by the program. A clock type system ensures that the program does not manipulate invalid data. In this paper, we establish an abstract type soundness result for synchronous languages: given a program, we can derive a system of set equations whose solution guarantees the absence of invalid data during execution. We then instantiate this result for synchronous languages with periodic clocks and show how to effectively solve the resulting set constraints. The development has been formalized in the Isabelle proof assistant.

Online Copy

Available as PDF

Isabelle sources

Available as gzip'ed tar file clock_type_soundness.tgz for Isabelle2012

BibTeX Entry

  author =       {Martin Strecker},
  title =        {Clock type soundness in synchronous languages},
  booktitle = {Proceedings of Dagstuhl Seminar 09481},
  year =      2009,
  editor =    {Albert Benveniste and Stephen A. Edwards and Edward Lee and Klaus Schneider and Reinhard von Hanxleden},
  url = {https://www.irit.fr/~Martin.Strecker/Publications/clock_type_soundness.html}

Last modified: Wed Dec 19 21:30:01 CET 2012