Sun 23 Jun 2019 09:00 - 09:45 at 106B - Interaction Trees and Algebraic Effects II Chair(s): Steve Zdancewic

Many software systems interact with their environment: a typical application creates files, send datagrams through network sockets, and more generally traverses many software layers to achieve basic effectful mechanisms. To get strong guarantees about the execution of these systems, one can implement a software stack from the ground up using a proof assistant like Coq and prove every desired property along the way.

Another plan would be to implement the system with a mixture of untrusted and certified modules, gradually extending the portion of certified code. This method shortens the path to getting runnable software but it requires modularity mechanisms for implementations, specifications, and proofs.

FreeSpec is a Coq library and plugin that offers that kind of modularity mechanisms to implement, to verify and to compose effectful components. In this talk, we will present these mechanisms as well as several applications ranging from building secure hardware architectures to UNIX-style standalone programs. This is joint work with Thomas Letan, Guillaume Hiet and Pierre Chifflier.

Sun 23 Jun

Displayed time zone: Tijuana, Baja California change

09:00 - 10:30
Interaction Trees and Algebraic Effects IIDeepSpec at 106B
Chair(s): Steve Zdancewic University of Pennsylvania
Implementation and Verification of Modular Effectful Systems in Coq using FreeSpec
Yann Régis-Gianas IRIF, University Paris Diderot and CNRS, France / INRIA PI.R2
Names, Places, and Things: Generic Traversals over Generic Syntax with Binding
James McKinna University of Edinburgh