Export to

• Google Calendar
• iCalendar file
• hCalendar markup
  <div class="vevent h-event"> <h1 class="summary p-name">Galois Tech Talk: Datatype Generic Packet Descriptions</h1> <div class='date'><time class="dtstart dt-start" title="2017-06-02T11:00:00" datetime="2017-06-02T11:00:00">Friday, June 2, 2017 from 11am</time>–<time class="dtend dt-end" title="2017-06-02T12:00:00" datetime="2017-06-02T12:00:00">noon</time></div> <div class="location vcard p-location h-card"> <a class="url" href='http://calagator.org/venues/202394717'><span class='fn org p-name'>Galois Inc</span></a> <div class="adr p-adr h-adr"> <div class="street-address p-street-address">421 Sw 6th Ave Ste 300</div> <span class="locality p-locality">Portland</span> , <span class="region p-region">OR</span> <span class="postal-code p-postal-code">97204</span> <div class="country-name p-country-name">US</div> (<a href='https://maps.google.com/maps?q=421%20Sw%206th%20Ave%20Ste%20300,%20Portland%20OR%2097204%20US'>map</a>) </div> </div> <div class="description p-description"> <h2>Speaker:</h2> <p>Wouter Swierstra</p> <h2>Abstract:</h2> <p>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.</p> <h2>Bio:</h2> <p>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.</p> </div> <h3>Links</h3> <ul> <li><a class="url u-url" href="http://galois.com/blog/2017/05/datatype-generic-packet-descriptions/">Website</a></li> </ul> </div>