Dedukti school

Si vous êtes tombé sur cette page sans être l'un des membres qui donne un cours durant l'école Dedukti, peut-être que vous cherchez plutôt cette page.

Sinon, libre à vous de consulter les slides de cours qui suivent :

• Dedukti & Lambdapi - Frédéric Blanqui : Slide
• How to express a theory in Dedukti? - Gilles Dowek : Slide
• The case of cubical type theory - Bruno Barras :
• How to write a translator to Dedukti? The case of Agda. - Jesper Cockx and Thiago Felicissimo : Slide
• How to handle systems using automated theorem provers? - Guillaume Burel :
• Predicate subtyping with proof irrelevance - Gabriel Hondet : Slide (avec notes : ici )
• How I Learned to Stop Trusting and Implement Dedukti Myself? - Michael Färber : Slide
• Programming language semantics in Dedukti - Catherine Dubois and Amélie Ledein : PARTIE 2
• Translating proofs from one theory to another within Dedukti, and exporting a library from Dedukti - François Thiré :