Thursday 21 October 2021, 10:00 AM, room 1X59 and online: La confluence de règles dans les calculs d'ordre supérieur avec types dépendants, Jean-Pierre Jouannaud (deducteam).

Il s'agit de faire le point sur

- le choix de prouver la confluence dans le lambda calcul non-typé annoté

- la technique des diagrammes décroissants de van Oostrom

- une definition monotone et stable de la récriture d'ordre supérieur, avec des règles dont les membres gauches sont des patterns

- le résultat obtenu avec des régles lineaires gauches

- les problèmes en présence de règles non-linéaires gauches

- le résultat actuel

- ce qui reste a faire: implémentation, améliorations, plus ou moins simples, problème ouvert.