Réécriture pour la programmation et la preuve

Ce cours offre une introduction aux fondements de la réécriture en lien avec le calcul et la logique ainsi qu’à ses applications. Ces concepts sont étudiés et développés tant du point de vue des langages (compilation du filtrage et de la réécriture) que du point de vue des preuves (confluence, terminaison, etc.).

La première partie couvre les systèmes de réécriture de premier ordre et les concepts sous-jacents tels que le filtrage, les règles de réécriture et les stratégies. Des propriétés classiques telles que la terminaison et la confluence sont introduites et différentes techniques de preuve sont décrites et illustrée sur des exemples concrets. Dans la deuxième partie, nous montrons comment ces concepts peuvent être mis en pratique. Nous présentons deux langues différentes basées sur la réécriture, TOM et XSLT, et nous montrons comment ces languages peuvent être utilisées pour l’analyse et la transformation de programmes et de documents XML, respectivement.