Thursday 17 September 2020, 15:30, LSV + online: Définitions et preuves inductives en théorie des types dépendants, Amélie Ledein (M2 intern, deducteam).

L'objectif de cette séance de séminaire est de présenter les travaux que j'ai réalisés durant mon stage de M2. L'objectif de ce stage était d'ajouter la possibilité d'écrire des définitions inductives et de générer automatiquement des principes d'induction au sein de Lambdapi (ainsi que de générer automatiquement des règles de réécriture associées au principe d'induction).

Après une brève comparaison à Coq, j'aborderai comment nous avons résolu le problème pour des types inductifs avec des arguments du 1er ordre, potentiellement dépendants, dont certaines imbrications sont possibles. J'expliquerai ensuite comment nous sommes parvenus à obtenir un algorithme commun permettant d'obtenir ou bien le principe d'induction, ou bien les règles de réécriture associées. Enfin, je présenterai l'extension de cet algorithme aux types inductifs mutuellement définis.