Treffer: Un système de types pour CHR

Nous proposons un système de types général pour le langage des Constraint Handling Rules (CHRs), un langage de règles de réécriture destiné à l'implantation de solveurs de contraintes. Les CHRs étant en fait une extension de haut niveau d'un langage hôte, tel que Prolog ou Java, le système de types est ainsi paramétré par le système de types du langage hôte. Nous montrons la cohérence du système de types pour les CHRs par rapport à leur sémantique opérationnelle. Nous étudions également le cas particulier où le langage hôte est un langage de programmation en logique avec contraintes, typé avec le système de types prescriptif que nous avons développé dans nos précédents travaux. En particulier nous montrons que le système résultant est cohérent avec le modèle d'exécution étendu CLP+CHR. Ce système est implanté à travers une extension du logiciel TCLP de typage des programmes logiques avec contraintes. Nous exposons nos résultats expérimentaux sur la vérification des types de solveurs et programmes utilisant les CHRs, dont le logiciel TCLP lui-même.