ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic

Formal proofs of the meta-theory of programming calculi are important tools to develop a trust-worthy theoretical base. The meta-theory of systems with session types is delicate and error prone. I will talk about an approach to mechanise such proofs in the Coq proof assistant. In particular, I want to discuss some subtle aspects around the adequacy around a particular choice of representation, in particular some lessons learned in the process. And finally, offer a glimpse on the things we want to try in the future. This is joint work with Nobuko Yoshida.

Sat 6 Apr

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 10:30
Mechanising Proofs for Behavioural Types and ProcessesBEHAPI at S4 (BEHAPI)
Chair(s): Antonio Ravara NOVA University of Lisbon and NOVA LINCS
09:00
30m
Talk
A Theory of Contexts for Higher-Order Encodings of Process Algebras
BEHAPI
Ivan Scagnetto University of Udine
09:30
30m
Talk
Formalising session-typed languages without worries
BEHAPI
Wen Kokke University of Edinburgh
10:00
30m
Talk
Adventures in Formalising the Meta-Theory of Session Types
BEHAPI
Francisco Ferreira Imperial College London