Encodage des systèmes

Ce projet vise à développer l'interopérabilité entre les assistants de preuve basés sur la théorie des types dépendants en étudiant l'encodage des univers dans le cadre logique Dedukti et en développant des outils pour traduire effectivement les bibliothèques de preuve existantes vers Dedukti.

This project aims at developing the interoperability between proof assistants based on dependent type theory by studying the encoding of universes in the Dedukti logical framework, and developing tools to actually translate existing proof libraries to Dedukti., Nous accueillons les étudiants ayant des connaissances en logique et une certaine expérience avec un logiciel d'aide à la preuve ou un langage de programmation fonctionnelle. We welcome students having some background in logic and some experience with some proof assistant or some functional programming language.

Début de la thèse : 01/10/2026

Nature du financement

Précisions sur le financement

Programme UPSaclay-Taïwan 2026-2027

Présentation établissement et labo d'accueil

Université Paris-Saclay GS Informatique et sciences du numérique

Encodage des systèmes de types avec univers dans Dedukti // Encoding type systems with universes in Dedukti, Encodage des systèmes de types avec univers dans Dedukti // Encoding type systems with universes in Dedukti Mots clés types dépendants, réécriture, univers, Rocq, Dedukti dependent types, rewriting, universes, Rocq, Dedukti, Etablissement délivrant le doctorat Université Paris-Saclay GS Informatique et sciences du numérique Ecole doctorale 580 Sciences et Technologies de l'Information et de la Communication