|
1 @InProceedings{CoquandSiles12, |
|
2 author = {T.~Coquand and V.~Siles}, |
|
3 title = {{A} {D}ecision {P}rocedure for {R}egular {E}xpression {E}quivalence in {T}ype {T}heory}, |
|
4 booktitle = {Proc.~of the 1st Conference on Certified Programs and Proofs}, |
|
5 pages = {119--134}, |
|
6 year = {2011}, |
|
7 volume = {7086}, |
|
8 series = {LNCS} |
|
9 } |
|
10 |
|
11 @InProceedings{Asperti12, |
|
12 author = {A.~Asperti}, |
|
13 title = {{A} {C}ompact {P}roof of {D}ecidability for {R}egular {E}xpression {E}quivalence}, |
|
14 booktitle = {Proc.~of the 3rd International Conference on Interactive Theorem Proving}, |
|
15 pages = {283--298}, |
|
16 year = {2012}, |
|
17 volume = {7406}, |
|
18 series = {LNCS} |
|
19 } |
|
20 |
|
21 @InProceedings{LammichTuerk12, |
|
22 author = {P.~Lammich and T.~Tuerk}, |
|
23 title = {{A}pplying {D}ata {R}efinement for {M}onadic {P}rograms to {H}opcroft's {A}lgorithm}, |
|
24 booktitle = {Proc.~of the 3rd International Conference on Interactive Theorem Proving}, |
|
25 year = {2012}, |
|
26 volume = {7406}, |
|
27 series = {LNCS}, |
|
28 pages = {166--182} |
|
29 } |
|
30 |
|
31 @PhdThesis{Braibant12, |
|
32 author = {T.~Braibant}, |
|
33 title = {{K}leene {A}lgebras, {R}ewriting {M}odulo {AC}, and {C}ircuits in {C}oq}, |
|
34 school = {University of Grenoble}, |
|
35 year = {2012} |
|
36 } |
|
37 |
|
38 @incollection{Nipkow11, |
|
39 author = {T.~Nipkow}, |
|
40 title = {{G}auss-{J}ordan {E}limination for {M}atrices {R}epresented as {F}unctions}, |
|
41 booktitle = {The Archive of Formal Proofs}, |
|
42 editor = {G.~Klein and T.~Nipkow and L.~Paulson}, |
|
43 publisher = {\url{http://afp.sourceforge.net/entries/Gauss-Jordan-Elim-Fun.shtml}}, |
|
44 year = 2011, |
|
45 note = {Formal proof development}, |
|
46 ISSN = {2150-914x} |
|
47 } |
|
48 |
|
49 @Article{Haines69, |
|
50 author = {L.~H.~Haines}, |
|
51 title = {{O}n {F}ree {M}onoids {P}artially {O}rdered by {E}mbedding}, |
|
52 journal = {Journal of Combinatorial Theory}, |
|
53 year = {1969}, |
|
54 volume = {6}, |
|
55 pages = {94--98} |
|
56 } |
|
57 |
|
58 @inproceedings{Berghofer03, |
|
59 author = {S.~Berghofer}, |
|
60 title = {{A} {C}onstructive {P}roof of {H}igman's {L}emma in {I}sabelle}, |
|
61 booktitle = {In Proc. of the Workshop on Types}, |
|
62 year = {2003}, |
|
63 pages = {66--82}, |
|
64 series = {LNCS}, |
|
65 volume = {3085} |
|
66 } |
|
67 |
|
68 @article{Gasarch09, |
|
69 author = {S.~A.~Fenner and W.~I.~Gasarch and B.~Postow}, |
|
70 title = {{T}he {C}omplexity of {F}inding {SUBSEQ(A)}}, |
|
71 journal = {Theory of Computing Systems}, |
|
72 volume = {45}, |
|
73 number = {3}, |
|
74 year = {2009}, |
|
75 pages = {577-612} |
|
76 } |
|
77 |
|
78 @Book{Shallit08, |
|
79 author = {J.~Shallit}, |
|
80 title = {{A} {S}econd {C}ourse in {F}ormal {L}anguages and {A}utomata {T}heory}, |
|
81 publisher = {Cambridge University Press}, |
|
82 year = {2008} |
|
83 } |
|
84 |
|
85 @Unpublished{Rosenberg06, |
|
86 author = {A.~L.~Rosenberg}, |
|
87 title = {{A} {B}ig {I}deas {A}pproach to the {T}heory of {C}omputation}, |
|
88 note = {Course notes for CMPSCI 401 at the University of Massachusetts}, |
|
89 year = {2006} |
|
90 } |
|
91 |
|
92 @incollection{myhillnerodeafp11, |
|
93 author = {C.~Wu and X.~Zhang and C.~Urban}, |
|
94 title = {{T}he {M}yhill-{N}erode {T}heorem based on {R}egular {E}xpressions}, |
|
95 booktitle = {The Archive of Formal Proofs}, |
|
96 editor = {G.~Klein and T.~Nipkow and L.~Paulson}, |
|
97 publisher = {\url{http://afp.sourceforge.net/entries/Myhill-Nerode.shtml}}, |
|
98 month = Aug, |
|
99 year = 2011, |
|
100 note = {Formal proof development}, |
|
101 ISSN = {2150-914x} |
|
102 } |
|
103 |
|
104 @PhdThesis{Haftmann09, |
|
105 author = {F.~Haftmann}, |
|
106 title = {{C}ode {G}eneration from {S}pecifications in {H}igher-{O}rder {L}ogic}, |
|
107 school = {Technical University of Munich}, |
|
108 year = {2009} |
|
109 } |
|
110 |
|
111 @article{Harper99, |
|
112 author = {R.~Harper}, |
|
113 title = {{P}roof-{D}irected {D}ebugging}, |
|
114 journal = {Journal of Functional Programming}, |
|
115 volume = {9}, |
|
116 number = {4}, |
|
117 year = {1999}, |
|
118 pages = {463-469} |
|
119 } |
|
120 |
|
121 @article{Yi06, |
|
122 author = {K.~Yi}, |
|
123 title = {{E}ducational {P}earl: `{P}roof-{D}irected {D}ebugging' {R}evisited |
|
124 for a {F}irst-{O}rder {V}ersion}, |
|
125 journal = {Journal of Functional Programming}, |
|
126 volume = {16}, |
|
127 number = {6}, |
|
128 year = {2006}, |
|
129 pages = {663-670} |
|
130 } |
|
131 |
|
132 |
|
133 @Manual{PittsHOL4, |
|
134 title = {{S}yntax and {S}emantics}, |
|
135 author = {A.~M.~Pitts}, |
|
136 note = {Part of the documentation for the HOL4 system.} |
|
137 } |
|
138 |
|
139 @article{OwensReppyTuron09, |
|
140 author = {S.~Owens and J.~Reppy and A.~Turon}, |
|
141 title = {{R}egular-{E}xpression {D}erivatives {R}e-{E}xamined}, |
|
142 journal = {Journal of Functional Programming}, |
|
143 volume = 19, |
|
144 number = {2}, |
|
145 year = 2009, |
|
146 pages = {173--190} |
|
147 } |
|
148 |
|
149 |
|
150 |
|
151 @article{KraussNipkow11, |
|
152 author = {A.~Krauss and T.~Nipkow}, |
|
153 title = {{P}roof {P}earl: {R}egular {E}xpression {E}quivalence and {R}elation {A}lgebra}, |
|
154 journal = {Journal of Automated Reasoning}, |
|
155 volume = 49, |
|
156 number = {1}, |
|
157 year = {2012}, |
|
158 pages = {95--106} |
|
159 } |
|
160 |
|
161 @Book{Kozen97, |
|
162 author = {D.~Kozen}, |
|
163 title = {{A}utomata and {C}omputability}, |
|
164 publisher = {Springer Verlag}, |
|
165 year = {1997} |
|
166 } |
|
167 |
|
168 |
|
169 |
|
170 @InProceedings{Almeidaetal10, |
|
171 author = {J.~B.~Almeida and N.~Moriera and D.~Pereira and S.~M.~de Sousa}, |
|
172 title = {{P}artial {D}erivative {A}utomata {F}ormalized in {C}oq}, |
|
173 booktitle = {Proc.~of the 15th International Conference on Implementation |
|
174 and Application of Automata}, |
|
175 pages = {59-68}, |
|
176 year = {2010}, |
|
177 volume = {6482}, |
|
178 series = {LNCS} |
|
179 } |
|
180 |
|
181 @incollection{Constable00, |
|
182 author = {R.~L.~Constable and |
|
183 P.~B.~Jackson and |
|
184 P.~Naumov and |
|
185 J.~C.~Uribe}, |
|
186 title = {{C}onstructively {F}ormalizing {A}utomata {T}heory}, |
|
187 booktitle = {Proof, Language, and Interaction}, |
|
188 year = {2000}, |
|
189 publisher = {MIT Press}, |
|
190 pages = {213-238} |
|
191 } |
|
192 |
|
193 |
|
194 @techreport{Filliatre97, |
|
195 author = {J.-C. Filli\^atre}, |
|
196 institution = {LIP - ENS Lyon}, |
|
197 number = {97--04}, |
|
198 title = {{F}inite {A}utomata {T}heory in {C}oq: |
|
199 {A} {C}onstructive {P}roof of {K}leene's {T}heorem}, |
|
200 type = {Research Report}, |
|
201 year = {1997} |
|
202 } |
|
203 |
|
204 @article{OwensSlind08, |
|
205 author = {S.~Owens and K.~Slind}, |
|
206 title = {{A}dapting {F}unctional {P}rograms to {H}igher {O}rder {L}ogic}, |
|
207 journal = {Higher-Order and Symbolic Computation}, |
|
208 volume = {21}, |
|
209 number = {4}, |
|
210 year = {2008}, |
|
211 pages = {377--409} |
|
212 } |
|
213 |
|
214 @article{Brzozowski64, |
|
215 author = {J.~A.~Brzozowski}, |
|
216 title = {{D}erivatives of {R}egular {E}xpressions}, |
|
217 journal = {Journal of the ACM}, |
|
218 volume = {11}, |
|
219 number = {4}, |
|
220 year = {1964}, |
|
221 pages = {481--494}, |
|
222 publisher = {ACM} |
|
223 } |
|
224 |
|
225 @inproceedings{Nipkow98, |
|
226 author={T.~Nipkow}, |
|
227 title={{V}erified {L}exical {A}nalysis}, |
|
228 booktitle={Proc.~of the 11th International Conference on Theorem Proving in Higher Order Logics}, |
|
229 series={LNCS}, |
|
230 volume=1479, |
|
231 pages={1--15}, |
|
232 year=1998 |
|
233 } |
|
234 |
|
235 @inproceedings{BerghoferNipkow00, |
|
236 author={S.~Berghofer and T.~Nipkow}, |
|
237 title={{E}xecuting {H}igher {O}rder {L}ogic}, |
|
238 booktitle={Proc.~of the International Workshop on Types for Proofs and Programs}, |
|
239 year=2002, |
|
240 series={LNCS}, |
|
241 volume=2277, |
|
242 pages="24--40" |
|
243 } |
|
244 |
|
245 @book{HopcroftUllman69, |
|
246 author = {J.~E.~Hopcroft and |
|
247 J.~D.~Ullman}, |
|
248 title = {{F}ormal {L}anguages and {T}heir {R}elation to {A}utomata}, |
|
249 publisher = {Addison-Wesley}, |
|
250 year = {1969} |
|
251 } |
|
252 |
|
253 |
|
254 @inproceedings{BerghoferReiter09, |
|
255 author = {S.~Berghofer and |
|
256 M.~Reiter}, |
|
257 title = {{F}ormalizing the {L}ogic-{A}utomaton {C}onnection}, |
|
258 booktitle = {Proc.~of the 22nd International |
|
259 Conference on Theorem Proving in Higher Order Logics}, |
|
260 year = {2009}, |
|
261 pages = {147-163}, |
|
262 series = {LNCS}, |
|
263 volume = {5674} |
|
264 } |
|
265 |
|
266 @Article{Church40, |
|
267 author = {A.~Church}, |
|
268 title = {{A} {F}ormulation of the {S}imple {T}heory of {T}ypes}, |
|
269 journal = {Journal of Symbolic Logic}, |
|
270 year = {1940}, |
|
271 volume = {5}, |
|
272 number = {2}, |
|
273 pages = {56--68} |
|
274 } |
|
275 |
|
276 @ARTICLE{Antimirov95, |
|
277 author = {V.~Antimirov}, |
|
278 title = {{P}artial {D}erivatives of {R}egular {E}xpressions and |
|
279 {F}inite {A}utomata {C}onstructions}, |
|
280 journal = {Theoretical Computer Science}, |
|
281 year = {1995}, |
|
282 volume = {155}, |
|
283 pages = {291--319} |
|
284 } |
|
285 |
|
286 @ARTICLE{Brzozowski10, |
|
287 author = {J.~A.~Brzozowski}, |
|
288 title = {{Q}uotient {C}omplexity of {R}egular {L}anguages}, |
|
289 journal = {Journal of Automata, Languages and Combinatorics}, |
|
290 volume = {15}, |
|
291 number = {1/2}, |
|
292 pages = {71--89}, |
|
293 year = 2010 |
|
294 } |
|
295 |
|
296 @book{Sakarovitch09, |
|
297 author = {J.~Sakarovitch}, |
|
298 title = {{E}lements of {A}utomata {T}heory}, |
|
299 publisher = {Cambridge University Press}, |
|
300 year = {2009} |
|
301 } |
|
302 |
|
303 @inproceedings{WuZhangUrban11, |
|
304 author = {C.~Wu and X.~Zhang and C.~Urban}, |
|
305 title = {{A} {F}ormalisation of the {M}yhill-{N}erode {T}heorem based on {R}egular {E}xpressions |
|
306 ({P}roof {P}earl)}, |
|
307 booktitle = {Proc.~of the 2nd International Conference on Interactive Theorem Proving}, |
|
308 year = {2011}, |
|
309 pages = {341--356}, |
|
310 series = {LNCS}, |
|
311 volume = {6898} |
|
312 } |
|
313 |
|
314 |
|
315 |
|
316 |
|
317 |
|
318 @Article{Okhotin04, |
|
319 author = "A.~Okhotin", |
|
320 title = "{B}oolean {G}rammars", |
|
321 journal = "Information and Computation", |
|
322 pages = "19--48", |
|
323 year = "2004", |
|
324 number = "1", |
|
325 volume = "194" |
|
326 } |
|
327 |
|
328 @Article{KountouriotisNR09, |
|
329 title = "{W}ell-founded {S}emantics for {B}oolean {G}rammars", |
|
330 author = "V.~Kountouriotis and C.~Nomikos and P.~Rondogiannis", |
|
331 journal = "Information and Computation", |
|
332 year = "2009", |
|
333 number = "9", |
|
334 volume = "207", |
|
335 pages = "945--967" |
|
336 } |
|
337 |
|
338 |
|
339 @article{Leroy09, |
|
340 author = {X.~Leroy}, |
|
341 title = {{F}ormal {V}erification of a {R}ealistic {C}ompiler}, |
|
342 journal = {Communications of the ACM}, |
|
343 year = {2009}, |
|
344 volume = {52}, |
|
345 number = {7}, |
|
346 pages = {107--115} |
|
347 } |
|
348 |
|
349 |
|
350 @Unpublished{Might11, |
|
351 title = "{Y}acc is {D}ead", |
|
352 author = "M.~Might and D.~Darais", |
|
353 note = "To appear in {\it Proc.~of the 16th ACM International Conference on |
|
354 Functional Programming (ICFP)}", |
|
355 year = "2011" |
|
356 } |
|
357 |
|
358 @InProceedings{Ford04, |
|
359 author = "B.~Ford", |
|
360 title = "{P}arsing {E}xpression {G}rammars: {A} {R}ecognition-{B}ased |
|
361 {S}yntactic {F}oundation", |
|
362 booktitle = "Proc.~of the 31st ACM Symposium on Principles of Programming Languages (POPL)", |
|
363 year = "2004", |
|
364 pages = "111--122" |
|
365 } |
|
366 |
|
367 @InProceedings{Ford02, |
|
368 author = "B.~Ford", |
|
369 title = "{P}ackrat {P}arsing: : {S}imple, {P}owerful, {L}azy, {L}inear {T}ime, |
|
370 ({F}unctional {P}earl)", |
|
371 booktitle = "Proc.~of the 7th ACM International Conference on Functional Programming (ICFP)", |
|
372 year = "2002", |
|
373 pages = "36--47" |
|
374 |
|
375 } |
|
376 |
|
377 @InProceedings{WarthDM08, |
|
378 title = "{P}ackrat {P}arsers {C}an {S}upport {L}eft {R}ecursion", |
|
379 author = "A.~Warth and J.~R.~Douglass and T.~D.~Millstein", |
|
380 booktitle = "Proc. of the {ACM} Symposium on |
|
381 Partial Evaluation and Semantics-based Program |
|
382 Manipulation (PEPM)", |
|
383 year = "2008", |
|
384 pages = "103--110" |
|
385 } |
|
386 |
|
387 @Article{Earley70, |
|
388 author = "J.~Earley", |
|
389 title = "{A}n {E}fficient {C}ontext-{F}ree {P}arsing {A}lgorithm", |
|
390 journal = "Communications of the ACM", |
|
391 volume = "13", |
|
392 number = "2", |
|
393 pages = "94--102", |
|
394 year = "1970" |
|
395 } |
|
396 |
|
397 @Article{AycHor02, |
|
398 author = "J.~Aycock and R.~N.~Horspool", |
|
399 title = "{P}ractical {E}arley {P}arsing", |
|
400 journal = "The Computer Journal", |
|
401 volume = "45", |
|
402 number = "6", |
|
403 pages = "620--630", |
|
404 year = "2002", |
|
405 } |
|
406 |