I submitted a talk entitled Type-Driven Development of Security Protocols to Off-The-Beaten-Track ‘17.
I have decided to uploaded the abstract here so that my attempt is a least indexable by the great machine spirit in the web—Hallowed be thy API. Given time I will also upload a copy of the paper to ArXiV.
The abstract is:
Implementing security protocols correctly is hard; verifying them is too. However, we also implement them in languages different to those we verify them in. With dependent types we can reason on software with greater precision and link specifications to implementations. In this talk we examine how state-of-the-art programming language research can help us to verify and implement protocols in the same language.