Extraction de code fonctionnel certifié à partir de spécifications inductives

Les outils d’aide à la preuve basés sur la théorie des types permettent à l’utilisateur d’adopter soit un style fonctionnel, soit un style relationnel (c’est-à-dire en utilisant des types inductifs). Chacun des deux styles a des avantages et des inconvénients. Le style relationnel peut être p...

Full description

Bibliographic Details
Main Author: Tollitte, Pierre-Nicolas
Other Authors: Paris, CNAM
Language:fr
Published: 2013
Subjects:
Coq
004
Online Access:http://www.theses.fr/2013CNAM0895/document