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
Times are displayed in time zone: (GMT-07:00) Tijuana, Baja California change

09:00 - 10:30: DeepSpec 2019 - Interaction Trees and Algebraic Effects II at 106B
Chair(s): Steve ZdancewicUniversity of Pennsylvania
deepspec-2019-papers09:00 - 09:45
Yann Régis-GianasIRIF, University Paris Diderot and CNRS, France / INRIA PI.R2
deepspec-2019-papers09:45 - 10:30
James McKinnaUniversity of Edinburgh