+ −
+ −
+ −
@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{OkuiSuzuki2013,+ −
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}+ −
}+ −
+ −