442 %H |
442 %H |
443 |
443 |
444 @InProceedings{Haftmann-Wenzel:2006:classes, |
444 @InProceedings{Haftmann-Wenzel:2006:classes, |
445 author = {Florian Haftmann and Makarius Wenzel}, |
445 author = {Florian Haftmann and Makarius Wenzel}, |
446 title = {Constructive Type Classes in {Isabelle}}, |
446 title = {Constructive Type Classes in {Isabelle}}, |
447 year = 2006, |
447 year = 2006, |
448 note = {To appear} |
448 note = {To appear; \url{http://www4.in.tum.de/~haftmann/pdf/constructive_type_classes_haftmann_wenzel.pdf}} |
|
449 } |
|
450 |
|
451 @TechReport{Haftmann-Nipkow:2007:codegen, |
|
452 author = {Florian Haftmann and Tobias Nipkow}, |
|
453 title = {A Code Generator Framework for {Isabelle/HOL}}, |
|
454 year = 2007, |
|
455 note = {\url{http://www4.in.tum.de/~haftmann/pdf/codegen_isabelle_haftmann_nipkow_16pp.pdf}} |
449 } |
456 } |
450 |
457 |
451 @manual{isabelle-classes, |
458 @manual{isabelle-classes, |
452 author = {Florian Haftmann}, |
459 author = {Florian Haftmann}, |
453 title = {Haskell-style type classes with {Isabelle}/{Isar}}, |
460 title = {Haskell-style type classes with {Isabelle}/{Isar}}, |
454 institution = TUM, |
461 institution = TUM, |
455 note = {\url{http://isabelle.in.tum.de/doc/classes.pdf}}} |
462 note = {\url{http://isabelle.in.tum.de/doc/classes.pdf}} |
|
463 } |
456 |
464 |
457 @manual{isabelle-codegen, |
465 @manual{isabelle-codegen, |
458 author = {Florian Haftmann}, |
466 author = {Florian Haftmann}, |
459 title = {Code generation from Isabelle theories}, |
467 title = {Code generation from Isabelle theories}, |
460 institution = TUM, |
468 institution = TUM, |
461 note = {\url{http://isabelle.in.tum.de/doc/codegen.pdf}}} |
469 note = {\url{http://isabelle.in.tum.de/doc/codegen.pdf}} |
|
470 } |
462 |
471 |
463 @Book{halmos60, |
472 @Book{halmos60, |
464 author = {Paul R. Halmos}, |
473 author = {Paul R. Halmos}, |
465 title = {Naive Set Theory}, |
474 title = {Naive Set Theory}, |
466 publisher = {Van Nostrand}, |
475 publisher = {Van Nostrand}, |