SAVE THE DATE
Monday afternoon, june 25, 2018
Universality of Proofs in SaCLay
Laboratoire d’Informatique de Polytechnique, Turing building, meeting room Gilles Kahn. An ID is mandatory to access the building
Place: Laboratoire d’Informatique de Polytechnique, Turing building, meeting room Gilles Kahn. An ID is mandatory to access the building.
13:45 Coffee
14:00 Bruno Barras (Inria Saclay – Île-de-France, LSV)
An analysis of Bindlib
Bindlib is an OCaml library that handles binders. Its design has a focus on efficiency, but its implementation uses unsafe features. We investigate how this library could be used as an alternative to
abstract machines. This requires an analysis of the library regarding its soundness, by developing a simple Hoare-logic, and the complexity of its main functions. This talk is a progress report regarding these two goals.
15:00 Break
15:15 Raphaël Cauderlier (IRIF)
FoCaLiZe and Dedukti to the Rescue for Proof Interoperability
Numerous contributions have been made for some years to allow users to exchange formal proofs between different provers. The main propositions consist in ad hoc pointwise translations, e.g. between HOL Light and Isabelle in the Flyspeck project or uses of more or less complete certificates. We propose a methodology to combine proofs coming from different theorem provers. This methodology relies on the Dedukti logical framework as a common formalism in which proofs can be translated and combined. To relate the independently developed mathematical libraries used in proof assistants, we rely on the structuring features offered by FoCaLiZe, in particular parameterized modules and inheritance to build a formal library of transfer theorems. We finally illustrate this methodology on the Sieve of Eratosthenes, which we prove correct using HOL and Coq in combination.
16:15 Break
16:30 Discussion
– Scientific day in October 2018 (15 minutes)
– Future of UPSCaLe (5 minutes)
– Common projects (15 minutes)
17:10 End