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
Schedule
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.