Simulating Eilenberg Machines with a Reactive Engine: Formal Specification, Proof and Program Extraction.

Benoit Razet 1
1 SANSKRIT - Sanskrit Computational Linguistics
Inria Paris-Rocquencourt, Université d'Hyderabad
Abstract : Eilenberg machines have been introduced in 1974 in the field of formal language theory. They are finite automata for which the alphabet is interpreted by mathematical relations over an abstract set. They generalize many finite state machines. We consider in the present work a class of Eilenberg machines for which we provide an executable complete simulator. This program is described using the Coq specification language. The correction of the algorithm is also proved formally and mechanically verified using the Coq proof assistant. The Coq extraction code technology allows to translate the specification into executable OCaml code. The algorithm and proofs are inspired from the reactive engine of Gérard Huet.
Type de document :
Rapport
[Research Report] INRIA. 2008
Liste complète des métadonnées

Littérature citée [6 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00257352
Contributeur : Benoit Razet <>
Soumis le : jeudi 3 avril 2008 - 14:55:45
Dernière modification le : mardi 17 avril 2018 - 11:30:01
Document(s) archivé(s) le : mardi 21 septembre 2010 - 15:46:21

Fichiers

spec_fem.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00257352, version 2

Collections

Citation

Benoit Razet. Simulating Eilenberg Machines with a Reactive Engine: Formal Specification, Proof and Program Extraction.. [Research Report] INRIA. 2008. 〈inria-00257352v2〉

Partager

Métriques

Consultations de la notice

139

Téléchargements de fichiers

67