1 

     2 @Book{Kozen97,

     3   author = 	 {D.~Kozen},

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

     5   publisher = 	 {Springer Verlag},

     6   year = 	 {1997}

     7 }

     8 

     9 

    10 @inproceedings{Constable00,

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

    12                P.~B.~Jackson and

    13                P.~Naumov and

    14                J.~C.~Uribe},

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

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

    17   year      = {2000},

    18   pages     = {213-238}

    19 }

    20 

    21 

    22 @techreport{Filliatre97,

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

    24   institution = {LIP - ENS Lyon},

    25   number = {97--04},

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

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

    28   type = {Research Report},

    29   year = {1997}

    30 }

    31 

    32 @article{OwensSlind08,

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

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

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

    36   volume    = {21},

    37   number    = {4},

    38   year      = {2008},

    39   pages     = {377--409}

    40 }

    41 

    42 @article{Brzozowski64,

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

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

    45  journal = {J.~ACM},

    46  volume = {11},

    47  issue = {4},

    48  year = {1964},

    49  pages = {481--494},

    50  publisher = {ACM}

    51 }