Skip to Main content Skip to Navigation
Reports

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.
Document type :
Reports
Complete list of metadata

Cited literature [6 references]  Display  Hide  Download

https://hal.inria.fr/inria-00257352
Contributor : Benoit Razet <>
Submitted on : Thursday, April 3, 2008 - 2:55:45 PM
Last modification on : Thursday, March 5, 2020 - 4:54:59 PM
Long-term archiving on: : Tuesday, September 21, 2010 - 3:46:21 PM

Files

spec_fem.pdf
Files produced by the author(s)

Identifiers

  • 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⟩

Share

Metrics

Record views

204

Files downloads

112