The meeting will take place at LRI, in the PCRI building (650), room 465.
Program:
- 13:30: welcome coffee
- 14:00: Emilio Gallego (Mines ParisTech), « Data Interchange in the Coq system: experiments and practical applications »
We will present recent work on SerLIB/SerAPI, a data-serialization library for machine-to-machine interaction with the Coq proof assistant.
SerAPI is built upon two ideas: using OCaml types as the data-specification language, and exposing the Coq API for RPC by reifying it to an explicit DSL. This solves one of the most challenging problems large systems such as Coq face with regards to data-export: maintenability, and faithfulness. SerAPI also includes a minimal protocol for the construction and checking of proof documents.
We will first provide a technical overview of the project, to move on to present some actual use cases.
SerAPI is a user-driven project, and most of the features today are the result of actual demands from users. In particular, we will highlight 4 use cases: user-interfaces, mutation proving, machine learning, and kernel traces.
- 14:45: coffee break
- 15:00: Émilie Grienenberger (LSV), « Concept alignment : connectives and quantifiers in the export of HOL Light proofs to Dedukti »
- 15:30: Quentin Garchery (LRI), « How to explain Why3 »
- 16:00: coffee break
- 16:20: discussion