@Unpublished{KraussNipkow11, author = {A.~Kraus and T.~Nipkow}, title = {{P}roof {P}earl: {R}egular {E}xpression {E}quivalence and {R}elation {A}lgebra}, note = {To appear in Journal of Automated Reasoning}, year = {2011}}@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={Proc.~of the 11th International Conference on Theorem Proving in Higher Order Logics}, series={LNCS}, volume=1479, pages={1--15}, year=1998}@inproceedings{BerghoferNipkow00, author={S.~Berghofer and T.~Nipkow}, title={{E}xecuting {H}igher {O}rder {L}ogic}, booktitle={Types for Proofs and Programs (TYPES 2000)}, year=2002, series=LNCS, volume=2277, pages="24--40"}@book{HopcroftUllman69, author = {J.~E.~Hopcroft and J.~D.~Ullman}, title = {{F}ormal {L}anguages and {T}heir {R}elation to {A}utomata}, publisher = {Addison-Wesley}, year = {1969}}@inproceedings{BerghoferReiter09, author = {S.~Berghofer and M.~Reiter}, title = {{F}ormalizing the {L}ogic-{A}utomaton {C}onnection}, booktitle = {Proc.~of the 22nd International Conference on Theorem Proving in Higher Order Logics}, year = {2009}, pages = {147-163}, series = LNCS, volume = {5674}}