Propositions-as-types (PaT) goes back to the functional interpretation of intuitionistic logic due to Brouwer, Heyting and Kolmogorov, but was brought under the spotlight only after the famous notes of Curry and Howard. It has been since then considered both an intriguing and prolific concept, with many instances and consequences in logic and the foundations of programming languages. In 2010 we have (with Pfenning) developed for the first time a PaT interpretation of linear logic which yields an expressive session-based programming language, while ensuring ("for-free") progress (deadlock-freedom), confluence, and normalisation as a consequence of the correspondence between computation and proof reduction. In this talk, we review this line of work and glimpse at some recent developments (with Rocha) on PaT and shared state.
Join at http://imt.lu/seminar