Datatype Generic Packet Descriptions

  • Date Friday, June 02, 2017  Time 11:00 AM
  • Speaker Wouter Swierstra
  • Location Galois Inc, 421 SW 6th Ave. Suite 300, Portland, OR, USA, (3rd floor of the Commonwealth building)
  • Galois is pleased to host the following tech talk.
    These talks are open to the interested public--please join us!
    (There is no need to pre-register for the talk.)


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.


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.