128 %B |
128 %B |
129 |
129 |
130 @book{Baader-Nipkow,author={Franz Baader and Tobias Nipkow}, |
130 @book{Baader-Nipkow,author={Franz Baader and Tobias Nipkow}, |
131 title="Term Rewriting and All That",publisher=CUP,year=1998} |
131 title="Term Rewriting and All That",publisher=CUP,year=1998} |
132 |
132 |
|
133 @manual{isabelle-locale, |
|
134 author = {Clemens Ballarin}, |
|
135 title = {Tutorial to Locales and Locale Interpretation}, |
|
136 institution = TUM, |
|
137 note = {\url{http://isabelle.in.tum.de/doc/locales.pdf}} |
|
138 } |
|
139 |
133 @InCollection{Barendregt-Geuvers:2001, |
140 @InCollection{Barendregt-Geuvers:2001, |
134 author = {H. Barendregt and H. Geuvers}, |
141 author = {H. Barendregt and H. Geuvers}, |
135 title = {Proof Assistants using Dependent Type Systems}, |
142 title = {Proof Assistants using Dependent Type Systems}, |
136 booktitle = {Handbook of Automated Reasoning}, |
143 booktitle = {Handbook of Automated Reasoning}, |
137 publisher = {Elsevier}, |
144 publisher = {Elsevier}, |
506 series = {LNCS}, |
513 series = {LNCS}, |
507 volume = {4502}, |
514 volume = {4502}, |
508 year = {2007} |
515 year = {2007} |
509 } |
516 } |
510 |
517 |
511 @TechReport{Haftmann-Nipkow:2007:codegen, |
518 @inproceedings{Haftmann-Nipkow:2010:code, |
512 author = {Florian Haftmann and Tobias Nipkow}, |
519 author = {Florian Haftmann and Tobias Nipkow}, |
513 title = {A Code Generator Framework for {Isabelle/HOL}}, |
520 title = {Code Generation via Higher-Order Rewrite Systems}, |
514 editor = {Klaus Schneider and Jens Brandt}, |
521 booktitle = {Functional and Logic Programming: 10th International Symposium: FLOPS 2010}, |
515 booktitle = {Theorem Proving in Higher Order Logics: Emerging Trends Proceedings}, |
522 year = 2010, |
516 month = {08}, |
523 publisher = {Springer}, |
517 year = {2007}, |
524 series = {Lecture Notes in Computer Science}, |
518 institution = {Department of Computer Science, University of Kaiserslautern}, |
525 editor = {Matthias Blume and Naoki Kobayashi and Germ{\'a}n Vidal}, |
519 number = {364/07} |
526 volume = {6009} |
520 } |
527 } |
521 |
528 |
522 @InProceedings{Haftmann-Wenzel:2009, |
529 @InProceedings{Haftmann-Wenzel:2009, |
523 author = {Florian Haftmann and Makarius Wenzel}, |
530 author = {Florian Haftmann and Makarius Wenzel}, |
524 title = {Local theory specifications in {Isabelle/Isar}}, |
531 title = {Local theory specifications in {Isabelle/Isar}}, |