Raisonnement certifié sur les nombres réels et les objets en théorie des types co-inductifs

Certified reasoning on real numbers and objects in co-inductive type theory

Alberto Ciaffaglione (1)

1 LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications

We adopt Formal Methods based on Type Theory for reasoning on the semantics of computer programs: the ultimate goal is to prove that a fragment of software meets its formal specification. Application areas of our research are the Real Numbers datatype and the Object-oriented Languages based on Objects. In the first part we construct the Real Numbers using streams, i.e. infinite sequences, of signed digits. We implement the Reals in Coq using streams, which are managed using coinductive judgments and corecursive algorithms. Then we introduce a constructive axiomatization and we use it for proving the adequacy of our construction. In the second part we approach Object-based Calculi with side-effects, focusing on Abadi and Cardelli's imp[sigma]. We reformulate imp[sigma] using modern encoding techniques, as Higher-Order Abstract Syntax and Coinductive proof systems in Natural Deduction style. Then we formalize imp[sigma] in Coq and we prove the Type Soundness.

Nous adoptons des Méthodes Formelles basées sur la Théorie de Type pour raisonner sur la sémantique des programmes: le but final est montrer qu'un fragment de logiciel répond à ses spécifications formelles. Les domaines d'application de notre recherche sont le type des données des Nombres Réels et les Langages orientés Objets. Dans la première partie nous construisons les réels en utilisant des streams, c.-à-d. des suites infinies, de chiffres signés. Nous mettons en application les Nombres Réels dans Coq en utilisant les streams, qui sont contrôlés en utilisant des jugements coinductifs et des algorithmes corecursifs. Puis nous présentons une axiomatisation constructive et nous l'employons pour prouver l'adéquation de notre construction. Dans la deuxième partie nous étudions les calculs basées objets avec effet de bord, nous concentrant sur imp[sigma] d'Abadi et de Cardelli. Nous reformulons imp[sigma] en utilisant des techniques de codage modernes, comme la Syntaxe Abstraite d'Ordre Supérieur et des systèmes de preuve Coinductifs en Déduction Naturelle. Enfin nous formalisons imp[sigma] dans Coq et nous prouvons la correction des types.

Mots clés: Fonctions récursives -- Informatique; Induction (logique); Théorie des types

Domaines: Autre [cs.OH]

Alberto Ciaffaglione. Certified reasoning on real numbers and objects in co-inductive type theory. Autre [cs.OH]. Institut National Polytechnique de Lorraine, 2003. Français. ⟨NNT : 2003INPL026N⟩. ⟨tel-01750193⟩