Skip to content

rocq-archive/automata

Folders and files

NameName
Last commit message
Last commit date

Latest commit

ce764e2 · Oct 20, 2018

History

20 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

This library, developed by J. Courant and J.C. Filliatre from ENS Paris,
formalises the beginning of formal language theory: finite automata
and rational languages, context-free grammars and push-down automata.

The main results are :

- every rational language is regular, i.e. for all rationnal language L there 
  exists a finite automata wich recognizes L (Lemma rat_is_reg in RatReg.v)

- for all context-free language L, there exists a push-down automata wich 
  recognizes L (Lemma equiv_APD_Gram in gram_aut.v)

- an example of classical result : if two languages are context-free, then 
  so is their union (Theorem union_is_LCF in gram5.v)

- the extraction of a parser generator. Errr...well... from the axiom we can 
  associate to every push-down automata a program recognizing the same 
  language (Theorem Parser1 in extract.v).

You can find a description of the modules in Modules.doc

Axioms.doc explains what are the remaining axioms in this work.

For further informations, send us a mail:

	[email protected]
	[email protected]