- Vivi Padova
- Il Bo
Giovedì 15 Settembre 2016 alle ore 15:00 in Aula 1C150, Jean-Pierre Jouannaud (Université Paris Saclay) terrà un seminario dal titolo “Engineering proof systems in Dedukti”.
There is an important need for formal proof in both mathematics (mathematical proofs using very large computations) and computer science (safe critical software).
Acceptance of both these needs by mathematicians and by the industry has been a very long process that can now be considered as completed. The main question left is to deliver the promisses that have been made.
Many different proof assistants have emerged, that try to answer these needs: AGDA, Coq, Elf, HOL, Isabelle, Matita, PVS,... ACL, ATP, FoCaLiZe, SAT, SMT...
Some of these systems have been used to carry out impressive proofs, some of twhich were too large to be carried out by humans. Here are a few: design and certification of the microkernel Sel4, of the C-compiler CompCert, of Hales theorem (Eurler's conjecture), and of Feit-Thompson theorem. These projects have been carried out with various proof assistants, all requiring several man-years. Their result is an Isabelle proof of Sel4, a Coq proof of COMPCert, an HOL proof of Euler’s conjecture, and a Coq proof of Feit-Thomson theorem.
Dedukti is a new proof assistant that allows to use proofs developped in your favourite system by translating them to proofs in Dedukti, which therefore appears as a common language for proof systems that enables their collaboration. Dedukti is based on an extension of the dependent type theorey LF by user-defined syntax and rewrite rules that serve encoding proofs.
This presentation will focus successively on:
- which proof systems can be encoded in Dedukti;
- the formal model underlying the design of Dedukti;
- an example: the encoding of Coq polymorphic universes in Dedukti;
- the format of rewrite rules, the properties they should satisfy, and how to check them.
Jean-Pierre Jouannaud graduated from Ecole Polytechnique de Paris and obtained his doctorate from University Paris 6 in 1978. He was then a professor successively at the universities of Nancy, then Paris-Sud, and finally at Ecole Polytechnique, in France, as well as an invited professor at a number of places, including Stanford Research Institute and Stanford University in US (2 years), the Polytechnicum University of Catalugna in Spain (1 year), and Tsinghua University in Beijing, China (5 years). He is now Professor emeritus at University Paris-Saclay in France.
Since the early 80’s, his research interests have been focusing on the interplay between deduction rules, rewrite rules, decision procedures, programming languages and type theory, in the development of programming languages (OBJ2), Rewriting tools (REVE), and of proof assistants (Coq, CoqMT and now Dedukti).