Por Peter Thiemann.
Abstract: Dependently-typed definitional interpreters offer a convenient way to define a language together with its type system such that type soundness of the language is guaranteed by the typing of the interpreter. This approach has been pursued extensively for functional languages. Recent work has addressed imperative languages with first-class references and objects.
Session types have emerged as a powerful paradigm for structuring communication-based programs. Type soundness proofs for language with session types are tedious and technically involved. It is rare to see mechanized soundness proofs for these systems.
We show that typed definitional interpretation is applicable to a multi-threaded functional language with communication primitives governed by session types by implementing a suitably typed interpreter in Agda. This implementation also provides a fully mechanized and executable soundness proof for the underlying session-typed calculus.
Short Bio: Peter Thiemann is a full professor of computer science at the University of Freiburg, Germany. His area of research is programming languages with an emphasis on functional programming, message-passing concurrency, and types. He has authored and co-authored more than 100 papers in this area. He served as a reviewer, pc member, pc chair, and general chair for various conferences including the flagship conference in this area, the ACM SIGPLAN International Conference on Functional Programming. He is an editor of the Journal of Functional Programming.
