A type system for hard real-time computation

Dan Ghica, University of Birmingham, Royaume-Uni

6 juin 2013 à 10H30, salle 1007 bâtiment Sophie Germain

Résumé: We will examine a type system, suitable for higher-order functional programming languages with mutable state, which can automatically certify the timing of execution. The system is generally applicable to hard real-time computation and especially to the automatic synthesis of computational pipelines. We present the general typing rules, a categorical semantic model and a proof of coherence as well as a concrete programming language with a type inference algorithm and a concrete game-semantic model. [Joint work with Alex Smith]