DEA Programmation: Sémantique, Preuves et Langages - Option Terminaison

Enseignants

• Jean-Pierre Jouannaud
• Claude Marché

Plan

Semaine 1 : 6 janvier-JPJ

Introduction, disponible en PDF

Semaine 2 : 13 janvier-JPJ

-

Semaine 3 : 20 janvier-JPJ

-

Semaine 4 : 27 janvier-JPJ

-

Semaine 5 : 3 février-JPJ

-

Semaine 6 : 10 février-CM

Terminaison de la réécriture du premier ordre, problématique de l'automatisation, de la modularité et de l'incrémentalité.

Semaine 7 : 17 février - pas de cours

Semaine 8 : 24 février-CM

Terminaison simple et terminaison CE.

Semaine 9 : 2 mars-CM

Résultats de modularité et d'incrémentalité.

Semaine 10 : 9 mars-CM

Incrémentalité et automatisation

Semaine 11 : 16 mars-CM

Terminaison de la réécriture conditionnelle, des programmes logiques, des programmes équationnels avec appartenance.

Lundi 5 avril

soutenances 9h-12h, salle a preciser

Notes de cours

• Preuves automatiques de terminaison

Choix d'articles a presenter

• Size-Change Termination for Term Rewriting Pris par Thierry Hubert
• Hierarchical termination revisited
• Argument Filtering Transformation Pris par Damien Pous q
• Approximating Dependency Graphs using Tree Automata Techniques Pris par Yann Regis-Gianas
• Dependency Pairs for Higher-Order Rewriting
• Polynomials for termination of context-sensitive rewriting Pris par Mathieu Hoyrup
• Dependency pairs for equational rewriting Pris par Boris Yakobowski
• Higher-order recursive path ordering "a la carte" (pour la partie qui traite des ordres modulo beta-eta qui n'ont pas ete traites en cours)
• Higher-Order Rewrite Systems and their Confluence
• Weak orthogonality implies confluence: the higher-order case
• Higher-Order Rewriting
• On Termination of Higher-Order Rewriting (version longue)

1. Contexte de l'article : quelle est la problématique, quelles sont les motivations.
2. Résultats principaux de l'article : énoncer les définitions importantes, énoncer les résultats nouveaux, éventuellement donner les preuves (en gros).
3. Critiquer l'article (au sens constructif du terme), comparer avec ce qui a été vu en cours.