@Unpublished{GasarchBlog,
author = {L.~Fortnow and W.~I.~Gasarch},
title = {{P}roving {DFA}-{L}angs {C}losed {U}nder {C}oncat and * {W}ithout {U}sing {E}quiv to
{NDFA's}},
note = {Retrieved \today, from \url{http://blog.computationalcomplexity.org}},
year = {2013}
}
@article{Gelade12,
author = {W.~Gelade and F.~Neven},
title = {{S}uccinctness of the {C}omplement and {I}ntersection of {R}egular
{E}xpressions},
journal = {ACM Transactions on Computational Logic},
volume = {13},
number = {1},
year = {2012},
pages = {4:1--4:21},
}
@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",
}
@InProceedings{Sulzmann12,
title = "M.~Sulzmann and K.~Z.~M.~Lu",
author = "XXX",
booktitle = "Proc. of XXX",
year = "2012",
pages = "XXX"
}