GitHub - rocq-archive/automata: Beginning of formal language theory

Branches Tags

Name		Name	Last commit message	Last commit date
Latest commit History 20 Commits
Axioms.doc		Axioms.doc
Dec.v		Dec.v
Ensf.v		Ensf.v
Ensf_couple.v		Ensf_couple.v
Ensf_dans.v		Ensf_dans.v
Ensf_disj.v		Ensf_disj.v
Ensf_inclus.v		Ensf_inclus.v
Ensf_inter.v		Ensf_inter.v
Ensf_map.v		Ensf_map.v
Ensf_produit.v		Ensf_produit.v
Ensf_types.v		Ensf_types.v
Ensf_union.v		Ensf_union.v
LICENSE		LICENSE
Make		Make
Makefile		Makefile
Max.v		Max.v
Modules.doc		Modules.doc
PushdownAutomata.v		PushdownAutomata.v
README		README
Rat.v		Rat.v
RatReg.v		RatReg.v
Reg.v		Reg.v
Relations.v		Relations.v
Words.v		Words.v
description		description
extract.v		extract.v
fonctions.v		fonctions.v
gram.v		gram.v
gram2.v		gram2.v
gram3.v		gram3.v
gram4.v		gram4.v
gram5.v		gram5.v
gram_aut.v		gram_aut.v
gram_g.v		gram_g.v
more_words.v		more_words.v
need.v		need.v

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:

	jcfillia@lip.ens-lyon.fr
	jcourant@lip.ens-lyon.fr