1st Dedukti school
Colocated with TYPES 2022.
Place: LS2N, Université de Nantes, Faculté des Sciences et Techniques (FST), Bâtiment 34, 2 Chemin de la Houssinière, 44322 Nantes, France.
The Dedukti school is preceded by the Women in EPN workshop from 9:00 to 13:30.
Program:
June 24, 2022:

14:3015:30 Dedukti & Lambdapi, Frédéric Blanqui will present the language Dedukti and the available tools for checking Dedukti files. He will also present Lambdapi, a new interactive proof assistant which can be used as an higherlevel intermediate language for generating Dedukti files.

15:3015:45 break

15:4516:45 How to express a theory in Dedukti? Gilles Dowek will present how simple theories, such as Predicate logic, Simple type theory, and the Calculus of constructions can be expressed in Dedukti, these expressions being the basis of the expression of more advances theories, such as the Calculus of constructions with universes and universe polymorphism, or cubical type theory can be expressed.

16:4517:15 The case of cubical type theory, Bruno Barras will describe a partial encoding of Cubical Type Theory in Dedukti. Beyond the mere interest of representing the features of that formalism, it is an example of a logic which definitional equality may not be representable as rewrite rules. We propose a general method to deal with issue.

17:1517:30 break

17:3019:00 WG 1 & 4 meeting: activities for November 2022  October 2023 ?

20:00 dinner
June 25, 2022:

9:0010:30 How to write a translator to Dedukti? The case of Agda. Jesper Cockx and Thiago Felicissimo will go over the basics of how to implement a translator from a proof assistant to Dedukti. We will start with the basic principles that can be applied in general for all proof assistants, before diving into our specific example: the case of the Agda translator, Agda2Dedukti. We will then look into three general features that exist in Agda as well as in other proof assistants based on type theory: inductive types with dependent pattern matching, universe polymorphism, and typedirected conversion rules for etaequality and definitional proof irrelevance. For each of these features, we will look into different ways to encode them and their respective benefits and downsides.

10:3010:45 break

10:4511:45 How to handle systems using automated theorem provers? Guillaume Burel will show how automated theorem provers (ATPs) can be used to obtain proofs for Dedukti. First, he will present how existing ATPs, namely Zenon Modulo, ArchSAT and iProverModulo, were instrumented to produce Dedukti proofs directly. Then, he will talk about systems that do not produce complete Dedukti proofs, but only traces describing coarsegrain steps like in the TSTP format. Complete Dedukti proofs can be reconstructed from such traces, using a tool like Ekstrakto and Deduktiproducing ATPs to fill out the missing details.

11:4512:15 Predicate subtyping with proof irrelevance, Gabriel Hondet will present an approach to push further the automation provided by Lambdapi to generate Dedukti specifications. In particular, we will see how userinput terms can be completed by the framework so that they are well typed. We will then consider this method to implement implicit predicate subtyping à la PVS in the framework.

13:3014:30 How I Learned to Stop Trusting and Implement Dedukti Myself? Michael Färber You should not need to trust the Dedukti developers in order to convince yourself that a Dedukti theory is correct. Michael Färber will give an overview of how Dedukti works internally and how to reimplement relevant parts of it yourself. In particular, he will touch upon parsing, terms, sharing, rewriting, and type checking. The goal of this talk is to empower anyone to write their own checker for Dedukti.

14:3015:30 Programming language semantics in Dedukti, Catherine Dubois and Amélie Ledein. Most systems that are translated into Dedukti are logical systems. This lecture will deviate a little from this type of systems and address the encoding in Dedukti of 1) some programming languages features like structural object subtyping, inheritance, method redefinition and late binding; 2) semantics definitions as they are provided by the K framework.

15:3015:45 break

15:4516:45 Translating proofs from one theory to another within Dedukti, and exporting a library from Dedukti, François Thiré will present a methodology to write proof translations in Dedukti based around two tools: Dkmeta allows to use the Dedukti language as a metalanguage to write term transformations that can be easily maintained; Universo allows to rewrite universes in a term, in particular, to map universes from one logic to another (when it is possible).
Registration: on the TYPES 2022 website
Funding applications: here (deadline: May 22)
Organizers: Gilles Dowek, Jesper Cockx, Frédéric Blanqui