|
1 |
|
2 |
|
3 |
|
4 @Misc{POSIX, |
|
5 title = {{T}he {O}pen {G}roup {B}ase {S}pecification {I}ssue 6 {IEEE} {S}td 1003.1 2004 {E}dition}, |
|
6 year = {2004}, |
|
7 note = {\url{http://pubs.opengroup.org/onlinepubs/009695399/basedefs/xbd_chap09.html}} |
|
8 } |
|
9 |
|
10 |
|
11 @InProceedings{AusafDyckhoffUrban2016, |
|
12 author = {F.~Ausaf and R.~Dyckhoff and C.~Urban}, |
|
13 title = {{POSIX} {L}exing with {D}erivatives of {R}egular {E}xpressions ({P}roof {P}earl)}, |
|
14 year = {2016}, |
|
15 booktitle = {Proc.~of the 7th International Conference on Interactive Theorem Proving (ITP)}, |
|
16 volume = {9807}, |
|
17 series = {LNCS}, |
|
18 pages = {69--86} |
|
19 } |
|
20 |
1 @article{aduAFP16, |
21 @article{aduAFP16, |
2 author = {Fahad Ausaf and Roy Dyckhoff and Christian Urban}, |
22 author = {F.~Ausaf and R.~Dyckhoff and C.~Urban}, |
3 title = {{POSIX} {L}exing with {D}erivatives of {R}egular {E}xpressions}, |
23 title = {{POSIX} {L}exing with {D}erivatives of {R}egular {E}xpressions}, |
4 journal = {Archive of Formal Proofs}, |
24 journal = {Archive of Formal Proofs}, |
5 year = 2016, |
25 year = 2016, |
6 note = {\url{http://www.isa-afp.org/entries/Posix-Lexing.shtml}, Formal proof development}, |
26 note = {\url{http://www.isa-afp.org/entries/Posix-Lexing.shtml}, Formal proof development}, |
7 ISSN = {2150-914x} |
27 ISSN = {2150-914x} |
253 year = {2010}, |
273 year = {2010}, |
254 volume = {6482}, |
274 volume = {6482}, |
255 series = {LNCS} |
275 series = {LNCS} |
256 } |
276 } |
257 |
277 |
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, |
278 @article{Owens2008, |
266 author = {S.~Owens and K.~Slind}, |
279 author = {S.~Owens and K.~Slind}, |
267 title = {{A}dapting {F}unctional {P}rograms to {H}igher {O}rder {L}ogic}, |
280 title = {{A}dapting {F}unctional {P}rograms to {H}igher {O}rder {L}ogic}, |
268 journal = {Higher-Order and Symbolic Computation}, |
281 journal = {Higher-Order and Symbolic Computation}, |
269 volume = {21}, |
282 volume = {21}, |
271 year = {2008}, |
284 year = {2008}, |
272 pages = {377--409} |
285 pages = {377--409} |
273 } |
286 } |
274 |
287 |
275 |
288 |
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, |
289 @article{Owens2, |
360 author = {Scott Owens and |
290 author = {S.~Owens and K.~Slind}, |
361 Konrad Slind}, |
|
362 title = {Adapting functional programs to higher order logic}, |
291 title = {Adapting functional programs to higher order logic}, |
363 journal = {Higher-Order and Symbolic Computation}, |
292 journal = {Higher-Order and Symbolic Computation}, |
364 volume = {21}, |
293 volume = {21}, |
365 number = {4}, |
294 number = {4}, |
366 pages = {377--409}, |
295 pages = {377--409}, |