@article{HosoyaVouillonPierce2005,
author = {H.~Hosoya and J.~Vouillon and B.~C.~Pierce},
title = {{R}egular {E}xpression {T}ypes for {XML}},
journal = {ACM Transactions on Programming Languages and Systems (TOPLAS)},
year = {2005},
volume = 27,
number = 1,
pages = {46--90}
}
@Misc{POSIX,
title = {{T}he {O}pen {G}roup {B}ase {S}pecification {I}ssue 6 {IEEE} {S}td 1003.1 2004 {E}dition},
year = {2004},
note = {\url{http://pubs.opengroup.org/onlinepubs/009695399/basedefs/xbd_chap09.html}}
}
@InProceedings{AusafDyckhoffUrban2016,
author = {F.~Ausaf and R.~Dyckhoff and C.~Urban},
title = {{POSIX} {L}exing with {D}erivatives of {R}egular {E}xpressions ({P}roof {P}earl)},
year = {2016},
booktitle = {Proc.~of the 7th International Conference on Interactive Theorem Proving (ITP)},
volume = {9807},
series = {LNCS},
pages = {69--86}
}
@article{aduAFP16,
author = {F.~Ausaf and R.~Dyckhoff and C.~Urban},
title = {{POSIX} {L}exing with {D}erivatives of {R}egular {E}xpressions},
journal = {Archive of Formal Proofs},
year = 2016,
note = {\url{http://www.isa-afp.org/entries/Posix-Lexing.shtml}, Formal proof development},
ISSN = {2150-914x}
}
@TechReport{CrashCourse2014,
author = {N.~B.~B.~Grathwohl and F.~Henglein and U.~T.~Rasmussen},
title = {{A} {C}rash-{C}ourse in {R}egular {E}xpression {P}arsing and {R}egular
{E}xpressions as {T}ypes},
institution = {University of Copenhagen},
year = {2014},
annote = {draft report}
}
@inproceedings{Sulzmann2014,
author = {M.~Sulzmann and K.~Lu},
title = {{POSIX} {R}egular {E}xpression {P}arsing with {D}erivatives},
booktitle = {Proc.~of the 12th International Conference on Functional and Logic Programming (FLOPS)},
pages = {203--220},
year = {2014},
volume = {8475},
series = {LNCS}
}
@inproceedings{Sulzmann2014b,
author = {M.~Sulzmann and P.~van Steenhoven},
title = {{A} {F}lexible and {E}fficient {ML} {L}exer {T}ool {B}ased on {E}xtended {R}egular
{E}xpression {S}ubmatching},
booktitle = {Proc.~of the 23rd International Conference on Compiler Construction (CC)},
pages = {174--191},
year = {2014},
volume = {8409},
series = {LNCS}
}
@book{Pierce2015,
author = {B.~C.~Pierce and C.~Casinghino and M.~Gaboardi and
M.~Greenberg and C.~Hri\c{t}cu and
V.~Sj\"{o}berg and B.~Yorgey},
title = {{S}oftware {F}oundations},
year = {2015},
publisher = {Electronic textbook},
note = {\url{http://www.cis.upenn.edu/~bcpierce/sf}}
}
@Misc{Kuklewicz,
author = {C.~Kuklewicz},
title = {{R}egex {P}osix},
howpublished = "\url{https://wiki.haskell.org/Regex_Posix}"
}
@article{Vansummeren2006,
author = {S.~Vansummeren},
title = {{T}ype {I}nference for {U}nique {P}attern {M}atching},
year = {2006},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {28},
number = {3},
pages = {389--428}
}
@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 (ITP)},
pages = {283--298},
year = {2012},
volume = {7406},
series = {LNCS}
}
@inproceedings{Frisch2004,
author = {A.~Frisch and L.~Cardelli},
title = {{G}reedy {R}egular {E}xpression {M}atching},
booktitle = {Proc.~of the 31st International Conference on Automata, Languages and Programming (ICALP)},
pages = {618--629},
year = {2004},
volume = {3142},
series = {LNCS}
}
@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}
}
@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 (TPHOLs)},
series={LNCS},
volume=1479,
pages={1--15},
year=1998
}
@article{Brzozowski1964,
author = {J.~A.~Brzozowski},
title = {{D}erivatives of {R}egular {E}xpressions},
journal = {Journal of the {ACM}},
volume = {11},
number = {4},
pages = {481--494},
year = {1964}
}
@article{Leroy2009,
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}
}
@InProceedings{Paulson2015,
author = {L.~C.~Paulson},
title = {{A} {F}ormalisation of {F}inite {A}utomata {U}sing {H}ereditarily {F}inite {S}ets},
booktitle = {Proc.~of the 25th International Conference on Automated Deduction (CADE)},
pages = {231--245},
year = {2015},
volume = {9195},
series = {LNAI}
}
@Article{Wu2014,
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},
journal = {Journal of Automatic Reasoning},
year = {2014},
volume = {52},
number = {4},
pages = {451--480}
}
@InProceedings{Regehr2011,
author = {X.~Yang and Y.~Chen and E.~Eide and J.~Regehr},
title = {{F}inding and {U}nderstanding {B}ugs in {C} {C}ompilers},
pages = {283--294},
year = {2011},
booktitle = {Proc.~of the 32nd ACM SIGPLAN Conference on Programming Language Design and
Implementation (PLDI)}
}
@Article{Norrish2014,
author = {A.~Barthwal and M.~Norrish},
title = {{A} {M}echanisation of {S}ome {C}ontext-{F}ree {L}anguage {T}heory in {HOL4}},
journal = {Journal of Computer and System Sciences},
year = {2014},
volume = {80},
number = {2},
pages = {346--362}
}
@Article{Thompson1968,
author = {K.~Thompson},
title = {{P}rogramming {T}echniques: {R}egular {E}xpression {S}earch {A}lgorithm},
journal = {Communications of the ACM},
issue_date = {June 1968},
volume = {11},
number = {6},
year = {1968},
pages = {419--422}
}
@article{Owens2009,
author = {S.~Owens and J.~H.~Reppy and A.~Turon},
title = {{R}egular-{E}xpression {D}erivatives {R}e-{E}xamined},
journal = {Journal of Functinal Programming},
volume = {19},
number = {2},
pages = {173--190},
year = {2009}
}
@inproceedings{Sulzmann2015,
author = {M.~Sulzmann and P.~Thiemann},
title = {{D}erivatives for {R}egular {S}huffle {E}xpressions},
booktitle = {Proc.~of the 9th International Conference on Language and Automata Theory
and Applications (LATA)},
pages = {275--286},
year = {2015},
volume = {8977},
series = {LNCS}
}
@inproceedings{Chen2012,
author = {H.~Chen and S.~Yu},
title = {{D}erivatives of {R}egular {E}xpressions and an {A}pplication},
booktitle = {Proc.~in the International Workshop on Theoretical
Computer Science (WTCS)},
pages = {343--356},
year = {2012},
volume = {7160},
series = {LNCS}
}
@article{Krauss2011,
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,
pages={95--106},
year=2012
}
@InProceedings{Traytel2015,
author = {D.~Traytel},
title = {{A} {C}oalgebraic {D}ecision {P}rocedure for {WS1S}},
booktitle = {Proc.~of the 24th Annual Conference on Computer Science Logic (CSL)},
pages = {487--503},
series = {LIPIcs},
year = {2015},
volume = {41}
}
@inproceedings{Traytel2013,
author={D.~Traytel and T.~Nipkow},
title={{A} {V}erified {D}ecision {P}rocedure for {MSO} on
{W}ords {B}ased on {D}erivatives of {R}egular {E}xpressions},
booktitle={Proc.~of the 18th ACM SIGPLAN International Conference on Functional Programming (ICFP)},
pages={3-12},
year=2013
}
@InProceedings{Coquand2012,
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 International Conference on Certified Programs and Proofs (CPP)},
pages = {119--134},
year = {2011},
volume = {7086},
series = {LNCS}
}
@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 (CIAA)},
pages = {59-68},
year = {2010},
volume = {6482},
series = {LNCS}
}
@article{Owens2008,
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{Owens2,
author = {S.~Owens and K.~Slind},
title = {Adapting functional programs to higher order logic},
journal = {Higher-Order and Symbolic Computation},
volume = {21},
number = {4},
pages = {377--409},
year = {2008},
url = {http://dx.doi.org/10.1007/s10990-008-9038-0},
doi = {10.1007/s10990-008-9038-0},
timestamp = {Wed, 16 Dec 2009 13:51:02 +0100},
biburl = {http://dblp.uni-trier.de/rec/bib/journals/lisp/OwensS08},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@misc{PCRE,
title = "{PCRE - Perl Compatible Regular Expressions}",
url = {http://www.pcre.org},
}
@InProceedings{OkuiSuzuki2010,
author = {S.~Okui and T.~Suzuki},
title = {{D}isambiguation in {R}egular {E}xpression {M}atching via
{P}osition {A}utomata with {A}ugmented {T}ransitions},
booktitle = {Proc.~of the 15th International Conference on Implementation
and Application of Automata (CIAA)},
year = {2010},
volume = {6482},
series = {LNCS},
pages = {231--240}
}
@TechReport{OkuiSuzukiTech,
author = {S.~Okui and T.~Suzuki},
title = {{D}isambiguation in {R}egular {E}xpression {M}atching via
{P}osition {A}utomata with {A}ugmented {T}ransitions},
institution = {University of Aizu},
year = {2013}
}
@inproceedings{Davis18,
author = {J.~C.~Davis and C.~.A.~Coghlan and F.~Servant and D.~Lee},
title = {{T}he {I}mpact of {R}egular {E}xpression {D}enial of {S}ervice ({ReDoS}) in
{P}ractice: {A}n {E}mpirical {S}tudy at the {E}cosystem {S}cale},
booktitle = {Proc.~of the 26th ACM Joint Meeting on European Software Engineering
Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE)},
year = {2018},
pages = {246--256},
numpages = {11}
}