diff -r 0679a84b11ad -r 01d223421ba0 Journal/Response/root.bib --- /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", +} +