@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}+ −
}+ −
+ −
@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 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}+ −
}+ −
+ −
@book{Michaelson,+ −
title={An introduction to functional programming through lambda calculus},+ −
author={Michaelson, Greg},+ −
year={2011},+ −
publisher={Courier Corporation}+ −
}+ −
+ −
@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}+ −
}+ −
+ −
+ −
@book{Velleman,+ −
title={How to prove it: a structured approach},+ −
author={Velleman, Daniel J},+ −
year={2006},+ −
publisher={Cambridge University Press}+ −
}+ −
+ −
@book{Jones,+ −
title={Implementing functional languages:[a tutorial]},+ −
author={Jones, Simon L Peyton and Lester, David R},+ −
volume={124},+ −
year={1992},+ −
publisher={Prentice Hall Reading}+ −
}+ −
+ −
@article{Cardelli,+ −
title={Type systems},+ −
author={Cardelli, Luca},+ −
journal={ACM Computing Surveys},+ −
volume={28},+ −
number={1},+ −
pages={263--264},+ −
year={1996}+ −
}+ −
+ −
@article{Morrisett,+ −
author = {J. Gregory Morrisett and+ −
Karl Crary and+ −
Neal Glew and+ −
David Walker},+ −
title = {Stack-based typed assembly language},+ −
journal = {J. Funct. Program.},+ −
volume = {13},+ −
number = {5},+ −
pages = {957--959},+ −
year = {2003},+ −
url = {http://dx.doi.org/10.1017/S0956796802004446},+ −
doi = {10.1017/S0956796802004446},+ −
timestamp = {Fri, 19 Mar 2004 13:48:27 +0100},+ −
biburl = {http://dblp.uni-trier.de/rec/bib/journals/jfp/MorrisettCGW03},+ −
bibsource = {dblp computer science bibliography, http://dblp.org}+ −
}+ −
+ −
@book{Nipkow,+ −
title={Concrete Semantics: With Isabelle/HOL},+ −
author={Nipkow, Tobias and Klein, Gerwin},+ −
year={2014},+ −
publisher={Springer}+ −
}+ −
+ −
@article{Dube,+ −
author = {Danny Dub{\'{e}} and+ −
Marc Feeley},+ −
title = {Efficiently building a parse tree from a regular expression},+ −
journal = {Acta Inf.},+ −
volume = {37},+ −
number = {2},+ −
pages = {121--144},+ −
year = {2000},+ −
url = {http://link.springer.de/link/service/journals/00236/bibs/0037002/00370121.htm},+ −
timestamp = {Tue, 25 Nov 2003 14:51:21 +0100},+ −
biburl = {http://dblp.uni-trier.de/rec/bib/journals/acta/DubeF00},+ −
bibsource = {dblp computer science bibliography, http://dblp.org}+ −
}+ −
+ −
@article{Morrisett2,+ −
author = {J. Gregory Morrisett and+ −
David Walker and+ −
Karl Crary and+ −
Neal Glew},+ −
title = {From system {F} to typed assembly language},+ −
journal = {{ACM} Trans. Program. Lang. Syst.},+ −
volume = {21},+ −
number = {3},+ −
pages = {527--568},+ −
year = {1999},+ −
url = {http://doi.acm.org/10.1145/319301.319345},+ −
doi = {10.1145/319301.319345},+ −
timestamp = {Wed, 26 Nov 2003 14:26:46 +0100},+ −
biburl = {http://dblp.uni-trier.de/rec/bib/journals/toplas/MorrisettWCG99},+ −
bibsource = {dblp computer science bibliography, http://dblp.org}+ −
}+ −
+ −
@article{Owens2,+ −
author = {Scott Owens and+ −
Konrad 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},+ −
}+ −
+ −
+ −
+ −