Implementation and Verification of Modular Effectful Systems in Coq using FreeSpec
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 JunDisplayed 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 | ||
09:00 45mTalk | Implementation and Verification of Modular Effectful Systems in Coq using FreeSpec DeepSpec Yann Régis-Gianas IRIF, University Paris Diderot and CNRS, France / INRIA PI.R2 | ||
09:45 45mTalk | Names, Places, and Things: Generic Traversals over Generic Syntax with Binding DeepSpec James McKinna University of Edinburgh |