By: Yann Régis-Gianas ( Paris University )
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.
Yann Régis-Gianas is an associate professor of Paris University, member of IRIF and of the PI.R2 Inria team that develops the Coq proof assistant. His field of research includes functional programming, type systems, certified programming, proof assistant implementation and design, and incremental programming.