Tuesday 6 October 2015, 10:00-19:00, ENS Cachan: Journée PML-Dedukti
Matin: auditorium CHEMLA, Institut d'Alembert.
PML est un langage de programmation en appel par valeurs similaire à ML, avec
une syntaxe à la Curry (c'est à dire, pas de types dans les termes) et basé
sur une logique d'ordre supérieur classique. Les termes apparaissent dans les
types via un prédicat d'appartenance t ∈ A et un opérateur de restriction
A | t = u. La sémantique de ces deux constructeurs de types utilise une
relation d'équivalence (observationnelle) sur les programmes (non typés).
L'opérateur de restriction est utile pour l'écriture de spécifications tandis
que l'appartenance permet d'encoder les types dépendants.
La présence de l'équivalence nous permet également de relâcher la "value
restriction" pour obtenir un type produit dépendant compatible avec la
logique classique (ce qui n'avait pas été fait avant).
Le système de type de PML intègre aussi une notion de sous-typage qui peut
être utilisée pour encoder des types (co-)inductifs.
Le "size-change principle" (SCP) est un algorithme simple donnant un test partiel de terminaison qui s'adapte très bien aux langages fonctionnels où les fonctions sont définies de manière récursive par pattern-matching.
En présence de constructeurs paresseux, le SCP donne également un test (partiel) de productivité : c'est sur ce principe que les tests (terminaison + productivité) de PML et Agda reposent.
Malheureusement, en présence de type coinductifs, certaines définitions récursives bien typées terminent (i.e. sont productives) mais sont incorrectes et rendent Agda/PML inconsistants.
En utilisant les travaux de L. Santocanale sur les preuves circulaires et les jeux de parité, je montrerais comment utiliser le SCP pour implanter un test partiel de totalité des définitions récursives qui généralise le test de terminaison/productivité, et garantie qu'une définition est correcte vis à vis de son type.
Après-midi: bibliothèque du LSV.