Deducteam's Interns Day 2022

Deducteam's Interns Day will take place on July 26 at ENS Paris-Saclay, room 3U42.

Amélie Rima, Taïssir Marce, Quentin Buzet and Elliot Butte will present their internship works. There will also be two extra talks, by Kazuhiko Sakaguchi and Thiago Felicissimo.

For any questions, please contact: thiago (dot) felicissimo (at) inria (dot) fr


Slots last 1h in order to allow for plenty of time for discussions and remarks. The beginning and end times are flexible and might vary from the schedule if needed.

The first four talks will be given in French, while the last two will be given in English.

9h30 - 10h30 : A categorical comparison between Church and primitve integers in System F, Amélie Rima

10h30 - 11h30 : Développement d'une bibliothèque standard sur les entiers naturels et les listes pour Lambdapi, Quentin Buzet

11h30 - 12h30 : Vers une traduction de Metamath en Dedukti, Elliot Butte

12h30 - 13h30 : Lunch

13h30 - 14h30 : Transformation de propositions dans Lambdapi, Taïssir Marce

14h30 - 15h30 : Reflexive tactics for algebra, revisited, Kazuhiko Sakaguchi

15h30 - 16h30 : Adequate and Computational Encodings in the Logical Framework Dedukti, Thiago Felicissimo

Abstracts of extra talks

Reflexive tactics for algebra, revisited, Kazuhiko Sakaguchi, accepted at ITP 2022

Abstract: Computational reflection allows us to turn verified decision procedures into efficient automated reasoning tools in proof assistants. The typical applications of such methodology include decidable algebraic theories such as equational theories of commutative rings and lattices. However, such existing tools are known not to cooperate with packed classes, a methodology to define mathematical structures in dependent type theory, that allows for the sharing of vocabulary across the inheritance hierarchy. Moreover, such tools do not support homomorphisms whose domain and codomain types may differ. This paper demonstrates how to implement reflexive tactics that support packed classes and homomorphisms. As applications of our methodology, we adapt the ring and field tactics of Coq to the commutative ring and field structures of the Mathematical Components library, and apply the resulting tactics to the formal proof of the irrationality of ζ(3) by Chyzak, Mahboubi, and Sibut-Pinote. As a result, the lines of code in the proof scripts have been reduced by 8%, and the time required for proof checking has been decreased by 27%.

Adequate and Computational Encodings in the Logical Framework Dedukti, Thiago Felicissimo, accepted at FSCD 2022

Abstract: Dedukti is a very expressive logical framework which unlike most frameworks, such as the Edinburgh Logical Framework (ELF), allows for the representation of computation alongside deduction. However, unlike ELF encodings, Dedukti encodings proposed until now do not feature an adequacy theorem --- i.e., a bijection between terms in the encoded system and in its encoding. Moreover, many of them also do not have a conservativity one, which compromises the ability of Dedukti to check proofs written in such encodings. We propose a different approach for Dedukti encodings which do not only allow for simpler conservativity proofs, but which also restore the adequacy of encodings. More precisely, we propose in this work adequate (and thus conservative) encodings for Functional Pure Type Systems. However, in contrast with ELF encodings, ours is computational --- that is, represents computation directly as computation. Therefore, our work is the first to present and prove correct an approach allowing for encodings that are both adequate and computational in Dedukti.