--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Journal/Response/root.bib Wed Dec 12 11:45:04 2012 +0000
@@ -0,0 +1,406 @@
+@InProceedings{CoquandSiles12,
+ author = {T.~Coquand and V.~Siles},
+ title = {{A} {D}ecision {P}rocedure for {R}egular {E}xpression {E}quivalence in {T}ype {T}heory},
+ booktitle = {Proc.~of the 1st Conference on Certified Programs and Proofs},
+ pages = {119--134},
+ year = {2011},
+ volume = {7086},
+ series = {LNCS}
+}
+
+@InProceedings{Asperti12,
+ author = {A.~Asperti},
+ title = {{A} {C}ompact {P}roof of {D}ecidability for {R}egular {E}xpression {E}quivalence},
+ booktitle = {Proc.~of the 3rd International Conference on Interactive Theorem Proving},
+ pages = {283--298},
+ year = {2012},
+ volume = {7406},
+ series = {LNCS}
+}
+
+@InProceedings{LammichTuerk12,
+ author = {P.~Lammich and T.~Tuerk},
+ title = {{A}pplying {D}ata {R}efinement for {M}onadic {P}rograms to {H}opcroft's {A}lgorithm},
+ booktitle = {Proc.~of the 3rd International Conference on Interactive Theorem Proving},
+ year = {2012},
+ volume = {7406},
+ series = {LNCS},
+ pages = {166--182}
+}
+
+@PhdThesis{Braibant12,
+ author = {T.~Braibant},
+ title = {{K}leene {A}lgebras, {R}ewriting {M}odulo {AC}, and {C}ircuits in {C}oq},
+ school = {University of Grenoble},
+ year = {2012}
+}
+
+@incollection{Nipkow11,
+ author = {T.~Nipkow},
+ title = {{G}auss-{J}ordan {E}limination for {M}atrices {R}epresented as {F}unctions},
+ booktitle = {The Archive of Formal Proofs},
+ editor = {G.~Klein and T.~Nipkow and L.~Paulson},
+ publisher = {\url{http://afp.sourceforge.net/entries/Gauss-Jordan-Elim-Fun.shtml}},
+ year = 2011,
+ note = {Formal proof development},
+ ISSN = {2150-914x}
+}
+
+@Article{Haines69,
+ author = {L.~H.~Haines},
+ title = {{O}n {F}ree {M}onoids {P}artially {O}rdered by {E}mbedding},
+ journal = {Journal of Combinatorial Theory},
+ year = {1969},
+ volume = {6},
+ pages = {94--98}
+}
+
+@inproceedings{Berghofer03,
+ author = {S.~Berghofer},
+ title = {{A} {C}onstructive {P}roof of {H}igman's {L}emma in {I}sabelle},
+ booktitle = {In Proc. of the Workshop on Types},
+ year = {2003},
+ pages = {66--82},
+ series = {LNCS},
+ volume = {3085}
+}
+
+@article{Gasarch09,
+ author = {S.~A.~Fenner and W.~I.~Gasarch and B.~Postow},
+ title = {{T}he {C}omplexity of {F}inding {SUBSEQ(A)}},
+ journal = {Theory of Computing Systems},
+ volume = {45},
+ number = {3},
+ year = {2009},
+ pages = {577-612}
+}
+
+@Book{Shallit08,
+ author = {J.~Shallit},
+ title = {{A} {S}econd {C}ourse in {F}ormal {L}anguages and {A}utomata {T}heory},
+ publisher = {Cambridge University Press},
+ year = {2008}
+}
+
+@Unpublished{Rosenberg06,
+ author = {A.~L.~Rosenberg},
+ title = {{A} {B}ig {I}deas {A}pproach to the {T}heory of {C}omputation},
+ note = {Course notes for CMPSCI 401 at the University of Massachusetts},
+ year = {2006}
+}
+
+@incollection{myhillnerodeafp11,
+ author = {C.~Wu and X.~Zhang and C.~Urban},
+ title = {{T}he {M}yhill-{N}erode {T}heorem based on {R}egular {E}xpressions},
+ booktitle = {The Archive of Formal Proofs},
+ editor = {G.~Klein and T.~Nipkow and L.~Paulson},
+ publisher = {\url{http://afp.sourceforge.net/entries/Myhill-Nerode.shtml}},
+ month = Aug,
+ year = 2011,
+ note = {Formal proof development},
+ ISSN = {2150-914x}
+}
+
+@PhdThesis{Haftmann09,
+ author = {F.~Haftmann},
+ title = {{C}ode {G}eneration from {S}pecifications in {H}igher-{O}rder {L}ogic},
+ school = {Technical University of Munich},
+ year = {2009}
+}
+
+@article{Harper99,
+ author = {R.~Harper},
+ title = {{P}roof-{D}irected {D}ebugging},
+ journal = {Journal of Functional Programming},
+ volume = {9},
+ number = {4},
+ year = {1999},
+ pages = {463-469}
+}
+
+@article{Yi06,
+ author = {K.~Yi},
+ title = {{E}ducational {P}earl: `{P}roof-{D}irected {D}ebugging' {R}evisited
+ for a {F}irst-{O}rder {V}ersion},
+ journal = {Journal of Functional Programming},
+ volume = {16},
+ number = {6},
+ year = {2006},
+ pages = {663-670}
+}
+
+
+@Manual{PittsHOL4,
+ title = {{S}yntax and {S}emantics},
+ author = {A.~M.~Pitts},
+ note = {Part of the documentation for the HOL4 system.}
+}
+
+@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}
+}
+
+
+
+@article{KraussNipkow11,
+ author = {A.~Krauss and T.~Nipkow},
+ title = {{P}roof {P}earl: {R}egular {E}xpression {E}quivalence and {R}elation {A}lgebra},
+ journal = {Journal of Automated Reasoning},
+ volume = 49,
+ number = {1},
+ year = {2012},
+ pages = {95--106}
+}
+
+@Book{Kozen97,
+ author = {D.~Kozen},
+ title = {{A}utomata and {C}omputability},
+ publisher = {Springer Verlag},
+ year = {1997}
+}
+
+
+
+@InProceedings{Almeidaetal10,
+ author = {J.~B.~Almeida and N.~Moriera and D.~Pereira and S.~M.~de Sousa},
+ title = {{P}artial {D}erivative {A}utomata {F}ormalized in {C}oq},
+ booktitle = {Proc.~of the 15th International Conference on Implementation
+ and Application of Automata},
+ pages = {59-68},
+ year = {2010},
+ volume = {6482},
+ series = {LNCS}
+}
+
+@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 = {Journal of the ACM},
+ volume = {11},
+ number = {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{Brzozowski10,
+ author = {J.~A.~Brzozowski},
+ 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
+}
+
+@book{Sakarovitch09,
+ author = {J.~Sakarovitch},
+ title = {{E}lements of {A}utomata {T}heory},
+ publisher = {Cambridge University Press},
+ year = {2009}
+}
+
+@inproceedings{WuZhangUrban11,
+ author = {C.~Wu and X.~Zhang and C.~Urban},
+ title = {{A} {F}ormalisation of the {M}yhill-{N}erode {T}heorem based on {R}egular {E}xpressions
+ ({P}roof {P}earl)},
+ booktitle = {Proc.~of the 2nd International Conference on Interactive Theorem Proving},
+ year = {2011},
+ pages = {341--356},
+ series = {LNCS},
+ volume = {6898}
+}
+
+
+
+
+
+@Article{Okhotin04,
+ author = "A.~Okhotin",
+ title = "{B}oolean {G}rammars",
+ journal = "Information and Computation",
+ pages = "19--48",
+ year = "2004",
+ number = "1",
+ volume = "194"
+}
+
+@Article{KountouriotisNR09,
+ title = "{W}ell-founded {S}emantics for {B}oolean {G}rammars",
+ author = "V.~Kountouriotis and C.~Nomikos and P.~Rondogiannis",
+ journal = "Information and Computation",
+ year = "2009",
+ number = "9",
+ volume = "207",
+ pages = "945--967"
+}
+
+
+@article{Leroy09,
+ author = {X.~Leroy},
+ title = {{F}ormal {V}erification of a {R}ealistic {C}ompiler},
+ journal = {Communications of the ACM},
+ year = {2009},
+ volume = {52},
+ number = {7},
+ pages = {107--115}
+}
+
+
+@Unpublished{Might11,
+ title = "{Y}acc is {D}ead",
+ author = "M.~Might and D.~Darais",
+ note = "To appear in {\it Proc.~of the 16th ACM International Conference on
+ Functional Programming (ICFP)}",
+ year = "2011"
+}
+
+@InProceedings{Ford04,
+ author = "B.~Ford",
+ title = "{P}arsing {E}xpression {G}rammars: {A} {R}ecognition-{B}ased
+ {S}yntactic {F}oundation",
+ booktitle = "Proc.~of the 31st ACM Symposium on Principles of Programming Languages (POPL)",
+ year = "2004",
+ pages = "111--122"
+}
+
+@InProceedings{Ford02,
+ author = "B.~Ford",
+ title = "{P}ackrat {P}arsing: : {S}imple, {P}owerful, {L}azy, {L}inear {T}ime,
+ ({F}unctional {P}earl)",
+ booktitle = "Proc.~of the 7th ACM International Conference on Functional Programming (ICFP)",
+ year = "2002",
+ pages = "36--47"
+
+}
+
+@InProceedings{WarthDM08,
+ title = "{P}ackrat {P}arsers {C}an {S}upport {L}eft {R}ecursion",
+ author = "A.~Warth and J.~R.~Douglass and T.~D.~Millstein",
+ booktitle = "Proc. of the {ACM} Symposium on
+ Partial Evaluation and Semantics-based Program
+ Manipulation (PEPM)",
+ year = "2008",
+ pages = "103--110"
+}
+
+@Article{Earley70,
+ author = "J.~Earley",
+ title = "{A}n {E}fficient {C}ontext-{F}ree {P}arsing {A}lgorithm",
+ journal = "Communications of the ACM",
+ volume = "13",
+ number = "2",
+ pages = "94--102",
+ year = "1970"
+}
+
+@Article{AycHor02,
+ author = "J.~Aycock and R.~N.~Horspool",
+ title = "{P}ractical {E}arley {P}arsing",
+ journal = "The Computer Journal",
+ volume = "45",
+ number = "6",
+ pages = "620--630",
+ year = "2002",
+}
+