Peer-Reviewed Book Chapters
Peer-Reviewed Conference and Workshop Papers
- Depending on Session-typed ProcessesMathematical Foundations of Programming Semantics, 2018
Session types are a typing discipline for message-passing concurrency that enables the specification of communication protocols as channel types, which can then be statically and/or dynamically enforced in order to ensure various correctness properties such as deadlock-freedom and protocol compliance.
However, in most session typing frameworks the language of types (and so, the language of protocols) is kept fairly limited, consisting mainly of sequential descriptions of input and output actions, combined with some form of branching or alternative behaviours.
In this talk I will present a dependent type theory, realised in a concurrent functional language based on the Curry-Howard interpretation of linear logic, that allows for session processes to depend on functions and vice-versa, as well as for the definition of type-level functions. By enriching the type language in this way, we are able to specify protocols where the choice of the next communication action can truly depend on the specific values of exchanged data – a significant gain in expressiveness wrt the state of the art. I will also show how the type theoretic nature of the framework allows us to internally describe and prove predicates on process behaviours, akin to dependently-typed specifications of functional programs.
Finally, in order to both justify some of our design choices and to benchmark the expressiveness of the theory I will introduce a faithful embedding (up-to the theory’s internal equality) of the functional layer of the calculus within the session-typed process layer.