@article{OwensReppyTuron09,

  author = {S.~Owens and J.~Reppy and A.~Turon},

  title = {{R}egular-{E}xpression {D}erivatives {R}e-{E}xamined},

  journal = {Journal of Functional Programming},

  volume = 19,

  number = {2},

  year = 2009,

  pages = {173--190}

}

@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}

}

@incollection{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},

  publisher = {MIT Press},

  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={Proc.~of the International Workshop on Types for Proofs and Programs},

  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}

}

@Article{Church40,

  author = 	 {A.~Church},

  title = 	 {{A} {F}ormulation of the {S}imple {T}heory of {T}ypes},

  journal = 	 {Journal of Symbolic Logic},

  year = 	 {1940},

  volume = 	 {5},

  number = 	 {2},

  pages = 	 {56--68}

}

@ARTICLE{Antimirov95,

    author = {V.~Antimirov},

    title = {{P}artial {D}erivatives of {R}egular {E}xpressions and 

     {F}inite {A}utomata {C}onstructions},

    journal = {Theoretical Computer Science},

    year = {1995},

    volume = {155},

    pages = {291--319}

}

@ARTICLE{Brozowski10,

  author = {J.~Brozowski},

  title = {{Q}uotient {C}omplexity of {R}egular {L}anguages},

  journal = {Journal of Automata, Languages and Combinatorics},

  volume = {15},

  number = {1/2}, 

  pages = {71--89},

  year = 2010