Place: ENS Cachan, IDA building, amphitheater Chemla (downstairs)

13:45 Coffee

14:00 Towards a Logic-Independent Proof Language, Florian Rabe (Erlangen and LRI)

While there is general agreement that system integration and interchange would benefit from a standardized system-independent language for proofs, a concrete definition remains elusive.

In this talk, I describe the requirements and challenges and summarize my current ideas for a solution.

Ideally this will generate a discussion that leads to the further refinement of these ideas.

rabe.pdf

15:00 Break

15:15 Translating an arithmetic library from Matita to HOL with Dedukti, François Thiré (Deducteam, LSV)

The aim of this work is to design an automatic but partial translation from Matita to HOL. This translation is not total since Matita is based on a variant of the Calculus of Inductive constructions, a logic more expressive than HOL. We identified three features of the logic behind Matita that does not exist in HOL that leads to three intermediate smaller translations namely: universes, dependent types and inductive types with recursive functions.

Using a logical framework such as Dedukti is handy here since it allows us to express all the intermediate logics between the transformations. Besides, we will see also that the rewrite engine of Dedukti can be used directly to express some of these transformations. We successfully applied this transformation to an arithmetic library that we were able to export in HOL.

thire.pdf

16:15 Break

16:30 Discussion

- New members (interns, PhD, postdoc, researchers) (5 minutes)

- Upscale budget (10 minutes)

- Submitted and granted projects (ANR, Europe, etc.) (5 minutes)

- Presentation of OpenDreamKit by Florian Rabe (10 minutes)

- Submitting projects together? (15 minutes)

17:15 End

GT Upscale

13:45 Coffee

14:00 Towards a Logic-Independent Proof Language, Florian Rabe (Erlangen and LRI)

While there is general agreement that system integration and interchange would benefit from a standardized system-independent language for proofs, a concrete definition remains elusive.

In this talk, I describe the requirements and challenges and summarize my current ideas for a solution.

Ideally this will generate a discussion that leads to the further refinement of these ideas.

rabe.pdf

15:00 Break

15:15 Translating an arithmetic library from Matita to HOL with Dedukti, François Thiré (Deducteam, LSV)

The aim of this work is to design an automatic but partial translation from Matita to HOL. This translation is not total since Matita is based on a variant of the Calculus of Inductive constructions, a logic more expressive than HOL. We identified three features of the logic behind Matita that does not exist in HOL that leads to three intermediate smaller translations namely: universes, dependent types and inductive types with recursive functions.

Using a logical framework such as Dedukti is handy here since it allows us to express all the intermediate logics between the transformations. Besides, we will see also that the rewrite engine of Dedukti can be used directly to express some of these transformations. We successfully applied this transformation to an arithmetic library that we were able to export in HOL.

thire.pdf

16:15 Break

16:30 Discussion

- New members (interns, PhD, postdoc, researchers) (5 minutes)

- Upscale budget (10 minutes)

- Submitted and granted projects (ANR, Europe, etc.) (5 minutes)

- Presentation of OpenDreamKit by Florian Rabe (10 minutes)

- Submitting projects together? (15 minutes)

17:15 End

GT Upscale