A type-theoretic foundation for programming with coroutines

In a seminal series of papers, Landin proposed in the sixties a direct translation (as opposed to a continuation-passing style translation) of an idealized Algol into the ?-calculus. This direct translation required to extend the ?-calculus with a new operator J in order to handle non-local jumps in Algol. This operator was the first control operators in functional languages (such as the famous call/cc of Scheme or Standard ML of New Jersey). A type system for control operators which extends the so-called Curry-Howard correspondence to classical logic first appeared in Griffin's pioneering work, and was immediately generalized to first-order dependent types (and Peano's arithmetic) by Murthy in his thesis. The following years, this extension of the formulas-as-types paradigm to classical logic has then studied by several researchers, but always in the context of functional programming. In [3], the authors thus decided to revisit Landin's work in the light of the computational interpretation of classical logic. More precisely, they extended the formulas-as-types notion of control to imperative programs with higher-order procedural mutable variables and non-local jumps. The resulting framework can be seen as a classical imperative type theory. Functional coroutines are a restricted form of control mechanism, where each continuation comes with its local environment. This restriction was originally obtained by considering a constructive version of Parigot's classical natural deduction [2]. A refinement of Krivine's abstract machine may also be defined and proved correct for functional coroutines. One thus obtain a very natural operational semantics for such coroutines. This thesis would consist in defining a type theory for imperative coroutines [5] based on a similar restriction of the classical imperative type theory, studying its properties and exploring some applications, such as for instance, an implementation of Kahn networks [4]. A comparative study with existing program logics for proving the correctness of coroutines is also expected [1].