@Book{Kozen97,
  author = 	 {D.~Kozen},
  title = 	 {{A}utomata and {C}omputability},
  publisher = 	 {Springer Verlag},
  year = 	 {1997}
}


@inproceedings{Constable00,
  author    = {R.~L.~Constable and
               P.~B.~Jackson and
               P.~Naumov and
               J.~C.~Uribe},
  title     = {{C}onstructively {F}ormalizing {A}utomata {T}heory},
  booktitle = {Proof, Language, and Interaction},
  year      = {2000},
  pages     = {213-238}
}


@techreport{Filliatre97,
  author = {J.-C. Filli\^atre},
  institution = {LIP - ENS Lyon},
  number = {97--04},
  title = {{F}inite {A}utomata {T}heory in {C}oq: 
           {A} {C}onstructive {P}roof of {K}leene's {T}heorem},
  type = {Research Report},
  year = {1997}
}

@article{OwensSlind08,
  author    = {S.~Owens and K.~Slind},
  title     = {{A}dapting {F}unctional {P}rograms to {H}igher {O}rder {L}ogic},
  journal   = {Higher-Order and Symbolic Computation},
  volume    = {21},
  number    = {4},
  year      = {2008},
  pages     = {377--409}
}

@article{Brzozowski64,
 author = {J.~A.~Brzozowski},
 title = {{D}erivatives of {R}egular {E}xpressions},
 journal = {J.~ACM},
 volume = {11},
 issue = {4},
 year = {1964},
 pages = {481--494},
 publisher = {ACM}
} 

@inproceedings{Nipkow98,
 author={T.~Nipkow},
 title={{V}erified {L}exical {A}nalysis},
 booktitle={Theorem Proving in Higher Order Logics},
 series=LNCS,
 volume=1479,
 pages={1--15},
 year=1998
}