La sémantique naturelle est un formalisme de description de sémantique opérationnelle. Au sein du système Centaur [1], ces descriptions sont directement exécutables via Typol, mais rien n'assure leur cohérence avant la phase de construction de l'interprête associé.
Il s'agit d'identifier les propriétés globales utiles pour assurer cette cohérence, puis de les exprimer en Coq [2] (système de manipulation de preuves mathématiques formelles). Il existe déjà un outil de traduction de spécifications Typol en définitions inductives Coq [3].
Ce sujet rentre dans le cadre d'une collaboration avec le projet Coq, INRIA Rocquencourt. Les travaux pourront être poursuivis en Thèse de Doctorat.
Encadrement : ATTALI, Isabelle
Téléphone : 04 92 38 79 10 Email : ia@sophia.inria.fr
Laboratoire ou équipe : INRIA Sophia Antipolis
Encadrement : PAULIN, Christine
Téléphone : 01 69 15 66 35 Email : Christine.Paulin@lri.fr
Laboratoire ou équipe : LRI, INRIA
Objectifs : Les objectifs du stage sont:
Prérequis : Sémantique, preuves
Matériel et logiciels utilisés : Stations de travail
INRIA Sophia Antipolis ou Rocquencourt