|
1 @article{aduAFP16, |
|
2 author = {Fahad Ausaf and Roy Dyckhoff and Christian Urban}, |
|
3 title = {{POSIX} {L}exing with {D}erivatives of {R}egular {E}xpressions}, |
|
4 journal = {Archive of Formal Proofs}, |
|
5 year = 2016, |
|
6 note = {\url{http://www.isa-afp.org/entries/Posix-Lexing.shtml}, Formal proof development}, |
|
7 ISSN = {2150-914x} |
|
8 } |
|
9 |
|
10 |
|
11 @TechReport{CrashCourse2014, |
|
12 author = {N.~B.~B.~Grathwohl and F.~Henglein and U.~T.~Rasmussen}, |
|
13 title = {{A} {C}rash-{C}ourse in {R}egular {E}xpression {P}arsing and {R}egular |
|
14 {E}xpressions as {T}ypes}, |
|
15 institution = {University of Copenhagen}, |
|
16 year = {2014}, |
|
17 annote = {draft report} |
|
18 } |
|
19 |
|
20 @inproceedings{Sulzmann2014, |
|
21 author = {M.~Sulzmann and K.~Lu}, |
|
22 title = {{POSIX} {R}egular {E}xpression {P}arsing with {D}erivatives}, |
|
23 booktitle = {Proc.~of the 12th International Conference on Functional and Logic Programming (FLOPS)}, |
|
24 pages = {203--220}, |
|
25 year = {2014}, |
|
26 volume = {8475}, |
|
27 series = {LNCS} |
|
28 } |
|
29 |
|
30 @inproceedings{Sulzmann2014b, |
|
31 author = {M.~Sulzmann and P.~van Steenhoven}, |
|
32 title = {{A} {F}lexible and {E}fficient {ML} {L}exer {T}ool {B}ased on {E}xtended {R}egular |
|
33 {E}xpression {S}ubmatching}, |
|
34 booktitle = {Proc.~of the 23rd International Conference on Compiler Construction (CC)}, |
|
35 pages = {174--191}, |
|
36 year = {2014}, |
|
37 volume = {8409}, |
|
38 series = {LNCS} |
|
39 } |
|
40 |
|
41 @book{Pierce2015, |
|
42 author = {B.~C.~Pierce and C.~Casinghino and M.~Gaboardi and |
|
43 M.~Greenberg and C.~Hri\c{t}cu and |
|
44 V.~Sj\"{o}berg and B.~Yorgey}, |
|
45 title = {{S}oftware {F}oundations}, |
|
46 year = {2015}, |
|
47 publisher = {Electronic textbook}, |
|
48 note = {\url{http://www.cis.upenn.edu/~bcpierce/sf}} |
|
49 } |
|
50 |
|
51 @Misc{Kuklewicz, |
|
52 author = {C.~Kuklewicz}, |
|
53 title = {{R}egex {P}osix}, |
|
54 howpublished = "\url{https://wiki.haskell.org/Regex_Posix}" |
|
55 } |
|
56 |
|
57 @article{Vansummeren2006, |
|
58 author = {S.~Vansummeren}, |
|
59 title = {{T}ype {I}nference for {U}nique {P}attern {M}atching}, |
|
60 year = {2006}, |
|
61 journal = {ACM Transactions on Programming Languages and Systems}, |
|
62 volume = {28}, |
|
63 number = {3}, |
|
64 pages = {389--428} |
|
65 } |
|
66 |
|
67 @InProceedings{Asperti12, |
|
68 author = {A.~Asperti}, |
|
69 title = {{A} {C}ompact {P}roof of {D}ecidability for {R}egular {E}xpression {E}quivalence}, |
|
70 booktitle = {Proc.~of the 3rd International Conference on Interactive Theorem Proving (ITP)}, |
|
71 pages = {283--298}, |
|
72 year = {2012}, |
|
73 volume = {7406}, |
|
74 series = {LNCS} |
|
75 } |
|
76 |
|
77 @inproceedings{Frisch2004, |
|
78 author = {A.~Frisch and L.~Cardelli}, |
|
79 title = {{G}reedy {R}egular {E}xpression {M}atching}, |
|
80 booktitle = {Proc.~of the 31st International Conference on Automata, Languages and Programming (ICALP)}, |
|
81 pages = {618--629}, |
|
82 year = {2004}, |
|
83 volume = {3142}, |
|
84 series = {LNCS} |
|
85 } |
|
86 |
|
87 @ARTICLE{Antimirov95, |
|
88 author = {V.~Antimirov}, |
|
89 title = {{P}artial {D}erivatives of {R}egular {E}xpressions and |
|
90 {F}inite {A}utomata {C}onstructions}, |
|
91 journal = {Theoretical Computer Science}, |
|
92 year = {1995}, |
|
93 volume = {155}, |
|
94 pages = {291--319} |
|
95 } |
|
96 |
|
97 @inproceedings{Nipkow98, |
|
98 author={T.~Nipkow}, |
|
99 title={{V}erified {L}exical {A}nalysis}, |
|
100 booktitle={Proc.~of the 11th International Conference on Theorem Proving in Higher Order Logics (TPHOLs)}, |
|
101 series={LNCS}, |
|
102 volume=1479, |
|
103 pages={1--15}, |
|
104 year=1998 |
|
105 } |
|
106 |
|
107 @article{Brzozowski1964, |
|
108 author = {J.~A.~Brzozowski}, |
|
109 title = {{D}erivatives of {R}egular {E}xpressions}, |
|
110 journal = {Journal of the {ACM}}, |
|
111 volume = {11}, |
|
112 number = {4}, |
|
113 pages = {481--494}, |
|
114 year = {1964} |
|
115 } |
|
116 |
|
117 @article{Leroy2009, |
|
118 author = {X.~Leroy}, |
|
119 title = {{F}ormal {V}erification of a {R}ealistic {C}ompiler}, |
|
120 journal = {Communications of the ACM}, |
|
121 year = 2009, |
|
122 volume = 52, |
|
123 number = 7, |
|
124 pages = {107--115} |
|
125 } |
|
126 |
|
127 @InProceedings{Paulson2015, |
|
128 author = {L.~C.~Paulson}, |
|
129 title = {{A} {F}ormalisation of {F}inite {A}utomata {U}sing {H}ereditarily {F}inite {S}ets}, |
|
130 booktitle = {Proc.~of the 25th International Conference on Automated Deduction (CADE)}, |
|
131 pages = {231--245}, |
|
132 year = {2015}, |
|
133 volume = {9195}, |
|
134 series = {LNAI} |
|
135 } |
|
136 |
|
137 @Article{Wu2014, |
|
138 author = {C.~Wu and X.~Zhang and C.~Urban}, |
|
139 title = {{A} {F}ormalisation of the {M}yhill-{N}erode {T}heorem based on {R}egular {E}xpressions}, |
|
140 journal = {Journal of Automatic Reasoning}, |
|
141 year = {2014}, |
|
142 volume = {52}, |
|
143 number = {4}, |
|
144 pages = {451--480} |
|
145 } |
|
146 |
|
147 @InProceedings{Regehr2011, |
|
148 author = {X.~Yang and Y.~Chen and E.~Eide and J.~Regehr}, |
|
149 title = {{F}inding and {U}nderstanding {B}ugs in {C} {C}ompilers}, |
|
150 pages = {283--294}, |
|
151 year = {2011}, |
|
152 booktitle = {Proc.~of the 32nd ACM SIGPLAN Conference on Programming Language Design and |
|
153 Implementation (PLDI)} |
|
154 } |
|
155 |
|
156 @Article{Norrish2014, |
|
157 author = {A.~Barthwal and M.~Norrish}, |
|
158 title = {{A} {M}echanisation of {S}ome {C}ontext-{F}ree {L}anguage {T}heory in {HOL4}}, |
|
159 journal = {Journal of Computer and System Sciences}, |
|
160 year = {2014}, |
|
161 volume = {80}, |
|
162 number = {2}, |
|
163 pages = {346--362} |
|
164 } |
|
165 |
|
166 @Article{Thompson1968, |
|
167 author = {K.~Thompson}, |
|
168 title = {{P}rogramming {T}echniques: {R}egular {E}xpression {S}earch {A}lgorithm}, |
|
169 journal = {Communications of the ACM}, |
|
170 issue_date = {June 1968}, |
|
171 volume = {11}, |
|
172 number = {6}, |
|
173 year = {1968}, |
|
174 pages = {419--422} |
|
175 } |
|
176 |
|
177 @article{Owens2009, |
|
178 author = {S.~Owens and J.~H.~Reppy and A.~Turon}, |
|
179 title = {{R}egular-{E}xpression {D}erivatives {R}e-{E}xamined}, |
|
180 journal = {Journal of Functinal Programming}, |
|
181 volume = {19}, |
|
182 number = {2}, |
|
183 pages = {173--190}, |
|
184 year = {2009} |
|
185 } |
|
186 |
|
187 @inproceedings{Sulzmann2015, |
|
188 author = {M.~Sulzmann and P.~Thiemann}, |
|
189 title = {{D}erivatives for {R}egular {S}huffle {E}xpressions}, |
|
190 booktitle = {Proc.~of the 9th International Conference on Language and Automata Theory |
|
191 and Applications (LATA)}, |
|
192 pages = {275--286}, |
|
193 year = {2015}, |
|
194 volume = {8977}, |
|
195 series = {LNCS} |
|
196 } |
|
197 |
|
198 @inproceedings{Chen2012, |
|
199 author = {H.~Chen and S.~Yu}, |
|
200 title = {{D}erivatives of {R}egular {E}xpressions and an {A}pplication}, |
|
201 booktitle = {Proc.~in the International Workshop on Theoretical |
|
202 Computer Science (WTCS)}, |
|
203 pages = {343--356}, |
|
204 year = {2012}, |
|
205 volume = {7160}, |
|
206 series = {LNCS} |
|
207 } |
|
208 |
|
209 @article{Krauss2011, |
|
210 author={A.~Krauss and T.~Nipkow}, |
|
211 title={{P}roof {P}earl: {R}egular {E}xpression {E}quivalence and {R}elation {A}lgebra}, |
|
212 journal={Journal of Automated Reasoning}, |
|
213 volume=49, |
|
214 pages={95--106}, |
|
215 year=2012 |
|
216 } |
|
217 |
|
218 @InProceedings{Traytel2015, |
|
219 author = {D.~Traytel}, |
|
220 title = {{A} {C}oalgebraic {D}ecision {P}rocedure for {WS1S}}, |
|
221 booktitle = {Proc.~of the 24th Annual Conference on Computer Science Logic (CSL)}, |
|
222 pages = {487--503}, |
|
223 series = {LIPIcs}, |
|
224 year = {2015}, |
|
225 volume = {41} |
|
226 } |
|
227 |
|
228 @inproceedings{Traytel2013, |
|
229 author={D.~Traytel and T.~Nipkow}, |
|
230 title={{A} {V}erified {D}ecision {P}rocedure for {MSO} on |
|
231 {W}ords {B}ased on {D}erivatives of {R}egular {E}xpressions}, |
|
232 booktitle={Proc.~of the 18th ACM SIGPLAN International Conference on Functional Programming (ICFP)}, |
|
233 pages={3-12}, |
|
234 year=2013 |
|
235 } |
|
236 |
|
237 @InProceedings{Coquand2012, |
|
238 author = {T.~Coquand and V.~Siles}, |
|
239 title = {{A} {D}ecision {P}rocedure for {R}egular {E}xpression {E}quivalence in {T}ype {T}heory}, |
|
240 booktitle = {Proc.~of the 1st International Conference on Certified Programs and Proofs (CPP)}, |
|
241 pages = {119--134}, |
|
242 year = {2011}, |
|
243 volume = {7086}, |
|
244 series = {LNCS} |
|
245 } |
|
246 |
|
247 @InProceedings{Almeidaetal10, |
|
248 author = {J.~B.~Almeida and N.~Moriera and D.~Pereira and S.~M.~de Sousa}, |
|
249 title = {{P}artial {D}erivative {A}utomata {F}ormalized in {C}oq}, |
|
250 booktitle = {Proc.~of the 15th International Conference on Implementation |
|
251 and Application of Automata (CIAA)}, |
|
252 pages = {59-68}, |
|
253 year = {2010}, |
|
254 volume = {6482}, |
|
255 series = {LNCS} |
|
256 } |
|
257 |
|
258 @book{Michaelson, |
|
259 title={An introduction to functional programming through lambda calculus}, |
|
260 author={Michaelson, Greg}, |
|
261 year={2011}, |
|
262 publisher={Courier Corporation} |
|
263 } |
|
264 |
|
265 @article{Owens2008, |
|
266 author = {S.~Owens and K.~Slind}, |
|
267 title = {{A}dapting {F}unctional {P}rograms to {H}igher {O}rder {L}ogic}, |
|
268 journal = {Higher-Order and Symbolic Computation}, |
|
269 volume = {21}, |
|
270 number = {4}, |
|
271 year = {2008}, |
|
272 pages = {377--409} |
|
273 } |
|
274 |
|
275 |
|
276 @book{Velleman, |
|
277 title={How to prove it: a structured approach}, |
|
278 author={Velleman, Daniel J}, |
|
279 year={2006}, |
|
280 publisher={Cambridge University Press} |
|
281 } |
|
282 |
|
283 @book{Jones, |
|
284 title={Implementing functional languages:[a tutorial]}, |
|
285 author={Jones, Simon L Peyton and Lester, David R}, |
|
286 volume={124}, |
|
287 year={1992}, |
|
288 publisher={Prentice Hall Reading} |
|
289 } |
|
290 |
|
291 @article{Cardelli, |
|
292 title={Type systems}, |
|
293 author={Cardelli, Luca}, |
|
294 journal={ACM Computing Surveys}, |
|
295 volume={28}, |
|
296 number={1}, |
|
297 pages={263--264}, |
|
298 year={1996} |
|
299 } |
|
300 |
|
301 @article{Morrisett, |
|
302 author = {J. Gregory Morrisett and |
|
303 Karl Crary and |
|
304 Neal Glew and |
|
305 David Walker}, |
|
306 title = {Stack-based typed assembly language}, |
|
307 journal = {J. Funct. Program.}, |
|
308 volume = {13}, |
|
309 number = {5}, |
|
310 pages = {957--959}, |
|
311 year = {2003}, |
|
312 url = {http://dx.doi.org/10.1017/S0956796802004446}, |
|
313 doi = {10.1017/S0956796802004446}, |
|
314 timestamp = {Fri, 19 Mar 2004 13:48:27 +0100}, |
|
315 biburl = {http://dblp.uni-trier.de/rec/bib/journals/jfp/MorrisettCGW03}, |
|
316 bibsource = {dblp computer science bibliography, http://dblp.org} |
|
317 } |
|
318 |
|
319 @book{Nipkow, |
|
320 title={Concrete Semantics: With Isabelle/HOL}, |
|
321 author={Nipkow, Tobias and Klein, Gerwin}, |
|
322 year={2014}, |
|
323 publisher={Springer} |
|
324 } |
|
325 |
|
326 @article{Dube, |
|
327 author = {Danny Dub{\'{e}} and |
|
328 Marc Feeley}, |
|
329 title = {Efficiently building a parse tree from a regular expression}, |
|
330 journal = {Acta Inf.}, |
|
331 volume = {37}, |
|
332 number = {2}, |
|
333 pages = {121--144}, |
|
334 year = {2000}, |
|
335 url = {http://link.springer.de/link/service/journals/00236/bibs/0037002/00370121.htm}, |
|
336 timestamp = {Tue, 25 Nov 2003 14:51:21 +0100}, |
|
337 biburl = {http://dblp.uni-trier.de/rec/bib/journals/acta/DubeF00}, |
|
338 bibsource = {dblp computer science bibliography, http://dblp.org} |
|
339 } |
|
340 |
|
341 @article{Morrisett2, |
|
342 author = {J. Gregory Morrisett and |
|
343 David Walker and |
|
344 Karl Crary and |
|
345 Neal Glew}, |
|
346 title = {From system {F} to typed assembly language}, |
|
347 journal = {{ACM} Trans. Program. Lang. Syst.}, |
|
348 volume = {21}, |
|
349 number = {3}, |
|
350 pages = {527--568}, |
|
351 year = {1999}, |
|
352 url = {http://doi.acm.org/10.1145/319301.319345}, |
|
353 doi = {10.1145/319301.319345}, |
|
354 timestamp = {Wed, 26 Nov 2003 14:26:46 +0100}, |
|
355 biburl = {http://dblp.uni-trier.de/rec/bib/journals/toplas/MorrisettWCG99}, |
|
356 bibsource = {dblp computer science bibliography, http://dblp.org} |
|
357 } |
|
358 |
|
359 @article{Owens2, |
|
360 author = {Scott Owens and |
|
361 Konrad Slind}, |
|
362 title = {Adapting functional programs to higher order logic}, |
|
363 journal = {Higher-Order and Symbolic Computation}, |
|
364 volume = {21}, |
|
365 number = {4}, |
|
366 pages = {377--409}, |
|
367 year = {2008}, |
|
368 url = {http://dx.doi.org/10.1007/s10990-008-9038-0}, |
|
369 doi = {10.1007/s10990-008-9038-0}, |
|
370 timestamp = {Wed, 16 Dec 2009 13:51:02 +0100}, |
|
371 biburl = {http://dblp.uni-trier.de/rec/bib/journals/lisp/OwensS08}, |
|
372 bibsource = {dblp computer science bibliography, http://dblp.org} |
|
373 } |
|
374 |
|
375 @misc{PCRE, |
|
376 title = "{PCRE - Perl Compatible Regular Expressions}", |
|
377 url = {http://www.pcre.org}, |
|
378 } |
|
379 |
|
380 |
|
381 |