Off The Beaten Track

Posted on November 11, 2016

Categories: idris, tdvcs, paper

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, warts and all, and regardless of whether it is accepted or not. Mainly so that it is a least indexable by the great machine spirit in the web---Hallowed be thy API.

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.