In G. Barthe and C. Fournet, editors, TGC'07, Sophia Antipolis, France, Lecture Notes in Computer Science, Springer Verlag, November 2007. Joint work with Ricardo Corin.
Distributed applications can be structured using sessions that specify flows of messages between roles. We design a small specific language to declare sessions. We then build a compiler, called s2ml, that transforms these declara- tions down to ML modules securely implementing the sessions. Every run of a well-typed program executing a session through its generated module is guaran- teed to follow the session specification, despite any low-level attempt by coali- tions of remote peers to deviate from their roles. We detail the inner workings of our compiler, along with our design choices, and illustrate the usage of s2ml with two examples: a simple remote procedure call session, and a complex ses- sion for a conference management system.
The slides from the TGC presentation in Sophia-Antipolis [pdf].