12 novembre 2012

Emmanuel Polonowski (LACL) salle des thèses

La formalisation à l’aide d’assistants de preuve des théories en sémantique des langages de programmation suppose de choisir une façon de représenter les lieurs de la syntaxe étudiée. Trois approches sont traditionnellement envisagées : une représentation par des variables nommées, une représentation par des indices de De Bruijn, une représentation par une syntaxe d’ordre supérieure. Chacune de ces approches possède un certain nombre d’avantages et d’inconvénients, et toutes ne peuvent être utilisées dans les différents assistants de preuve.

Nous présenterons dans cet exposé un outil permettant la génération automatique de fonctions et de propriétés nécessaires à la représentation sous forme d’indices de De Bruijn, qui évite au chercheur un développement souvent fastidieux et sans intérêt et lui laisse ainsi davantage de temps pour se concentrer sur les propriétés majeures de son travail. Nous verrons les points forts et les limites de cet outil, ainsi que plusieurs exemples d’utilisation et des informations sur sa conception.