Abstract:
Complex protocols describing the communication or storage of binary data are difficult to describe precisely. In this talk, I want to explore how to define data types describing a binary data formats and generate the corresponding serialization and deserialization functions from such descriptions. By embedding these data types in a general purpose dependently typed programming language such as Agda, we can verify once and for all that the serialization/deserialization functions generated in this style are correct by construction. To validate this approach, I will sketch how to write a verified parser for IPv4 network packets.
Bio:
Wouter Swierstra is an assistant professor at the Utrecht University in the Netherlands. After originally studying Mathematics and Computer Science, he did his PhD under supervision of Thorsten Altenkirch at the University of Nottingham’s Functional Programming Lab. He worked as a postdoc at Chalmers University of Technology, before moving back to the Netherlands to work at Vector Fabrics, a high-tech startup that used functional programming to facilitate the design of embedded systems. After this brief stint in industry, he returned to academia as a postdoc in Foundations Group at the Radboud University Nijmegen and Software Technology group at Utrecht University.