1 @article{OwensReppyTuron09,

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

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

     4   journal = {Journal of Functional Programming},

     5   volume = 19,

     6   number = {2},

     7   year = 2009,

     8   pages = {173--190}

     9 }

    10 

    11 

    12 

    13 @Unpublished{KraussNipkow11,

    14   author = 	 {A.~Kraus and T.~Nipkow},

    15   title = 	 {{P}roof {P}earl: {R}egular {E}xpression {E}quivalence and {R}elation {A}lgebra},

    16   note = 	 {To appear in Journal of Automated Reasoning},

    17   year = 	 {2011}

    18 }

    19 

    20 @Book{Kozen97,

    21   author = 	 {D.~Kozen},

    22   title = 	 {{A}utomata and {C}omputability},

    23   publisher = 	 {Springer Verlag},

    24   year = 	 {1997}

    25 }

    26 

    27 

    28 @incollection{Constable00,

    29   author    = {R.~L.~Constable and

    30                P.~B.~Jackson and

    31                P.~Naumov and

    32                J.~C.~Uribe},

    33   title     = {{C}onstructively {F}ormalizing {A}utomata {T}heory},

    34   booktitle = {Proof, Language, and Interaction},

    35   year      = {2000},

    36   publisher = {MIT Press},

    37   pages     = {213-238}

    38 }

    39 

    40 

    41 @techreport{Filliatre97,

    42   author = {J.-C. Filli\^atre},

    43   institution = {LIP - ENS Lyon},

    44   number = {97--04},

    45   title = {{F}inite {A}utomata {T}heory in {C}oq: 

    46            {A} {C}onstructive {P}roof of {K}leene's {T}heorem},

    47   type = {Research Report},

    48   year = {1997}

    49 }

    50 

    51 @article{OwensSlind08,

    52   author    = {S.~Owens and K.~Slind},

    53   title     = {{A}dapting {F}unctional {P}rograms to {H}igher {O}rder {L}ogic},

    54   journal   = {Higher-Order and Symbolic Computation},

    55   volume    = {21},

    56   number    = {4},

    57   year      = {2008},

    58   pages     = {377--409}

    59 }

    60 

    61 @article{Brzozowski64,

    62  author = {J.~A.~Brzozowski},

    63  title = {{D}erivatives of {R}egular {E}xpressions},

    64  journal = {J.~ACM},

    65  volume = {11},

    66  issue = {4},

    67  year = {1964},

    68  pages = {481--494},

    69  publisher = {ACM}

    70 } 

    71 

    72 @inproceedings{Nipkow98,

    73  author={T.~Nipkow},

    74  title={{V}erified {L}exical {A}nalysis},

    75  booktitle={Proc.~of the 11th International Conference on Theorem Proving in Higher Order Logics},

    76  series={LNCS},

    77  volume=1479,

    78  pages={1--15},

    79  year=1998

    80 }

    81 

    82 @inproceedings{BerghoferNipkow00,

    83   author={S.~Berghofer and T.~Nipkow},

    84   title={{E}xecuting {H}igher {O}rder {L}ogic},

    85   booktitle={Proc.~of the International Workshop on Types for Proofs and Programs},

    86   year=2002,

    87   series={LNCS},

    88   volume=2277,

    89   pages="24--40"

    90 }

    91 

    92 @book{HopcroftUllman69,

    93   author    = {J.~E.~Hopcroft and

    94                J.~D.~Ullman},

    95   title     = {{F}ormal {L}anguages and {T}heir {R}elation to {A}utomata},

    96   publisher = {Addison-Wesley},

    97   year      = {1969}

    98 }

    99 

   100 

   101 @inproceedings{BerghoferReiter09,

   102   author    = {S.~Berghofer and

   103                M.~Reiter},

   104   title     = {{F}ormalizing the {L}ogic-{A}utomaton {C}onnection},

   105   booktitle = {Proc.~of the 22nd International

   106                Conference on Theorem Proving in Higher Order Logics},

   107   year      = {2009},

   108   pages     = {147-163},

   109   series    = {LNCS},

   110   volume    = {5674}

   111 }