EMTST engineering the meta-theory of session types
File(s)DTRS19-4.pdf (803.98 KB)
Published version
Author(s)
Castro-Perez, D
Ferreira Ruiz, F
Yoshida, N
Type
Report
Abstract
Session types provide a principled programming discipline for structured interactions. They are used to statically check the safety of protocol composition and the absence of communication errors. These properties depend upon the meta-theory of the typing discipline, usually a type safety proof. These proofs, while conceptually simple, are very delicate and error prone due to the presence of linearity and name passing and have been falsified in several works in the literature. In this work, we explore mechanised proofs in theorem assistants as tools to develop trustworthy proofs, and at the same time to guide extensions that do not violate type safety. To that end, we study the meta-theory of two of the most used binary session types systems, the Honda-Vasconcelos-Kubo system and the more flexible revisited system by Yoshida and Vasconcelos. Additionally, we show the subtlety of representing the first system in α-equivalent representations.We develop these proofs in the Coq proof assistant, using a locally nameless representation for binders, and small scale reflection and overloaded lemmas to simplify the handling of linear typing environments.
Date Issued
2019-01-01
Publisher
Department of Computing, Imperial College London
Start Page
1
End Page
26
Journal / Book Title
Departmental Technical Report: 19/4
Copyright Statement
© 2019 The Author(s). This report is available open access under a CC-BY-NC-ND (https://creativecommons.org/licenses/by-nc-nd/4.0/)
Sponsor
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (E
Engineering and Physical Sciences Research Council
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (E
Grant Number
ERI 025567 (EP/K034413/1)
EP/K011715/1
EP/N027833/1
PO 20131167
EP/L00058X/1, PO 20131167
EP/T006544/1
PO 20263116
Publication Status
Published