YC_in_Coq
YC_in_Coq is a repository of definitions and proofs for formal language theory.
Our contribution
Intersection of CFG and DFA
Base2.v
ChomskyInduction.v
DFA.v
Intersection.v
Union.v
Generalized LL (GLL)
Definitions.v
GLL.v
Imported libs
Verified Algorithms for Context-Free Grammars in Coq
Some automata theory