431 crossref = {hug93}, |
431 crossref = {hug93}, |
432 pages = {141-154}} |
432 pages = {141-154}} |
433 |
433 |
434 %H |
434 %H |
435 |
435 |
|
436 @manual{isabelle-classes, |
|
437 author = {Florian Haftmann}, |
|
438 title = {Haskell-style type classes with {Isabelle}/{Isar}}, |
|
439 institution = TUM, |
|
440 note = {\url{http://isabelle.in.tum.de/doc/classes.pdf}}} |
|
441 |
|
442 @manual{isabelle-codegen, |
|
443 author = {Florian Haftmann}, |
|
444 title = {Code generation from Isabelle theories}, |
|
445 institution = TUM, |
|
446 note = {\url{http://isabelle.in.tum.de/doc/codegen.pdf}}} |
|
447 |
436 @Book{halmos60, |
448 @Book{halmos60, |
437 author = {Paul R. Halmos}, |
449 author = {Paul R. Halmos}, |
438 title = {Naive Set Theory}, |
450 title = {Naive Set Theory}, |
439 publisher = {Van Nostrand}, |
451 publisher = {Van Nostrand}, |
440 year = 1960} |
452 year = 1960} |
513 author = {J. Harrison}, |
525 author = {J. Harrison}, |
514 title = {A {Mizar} Mode for {HOL}}, |
526 title = {A {Mizar} Mode for {HOL}}, |
515 pages = {203--220}, |
527 pages = {203--220}, |
516 crossref = {tphols96}} |
528 crossref = {tphols96}} |
517 |
529 |
|
530 %J |
|
531 |
|
532 @article{haskell-revised-report, |
|
533 author = {Simon {Peyton Jones} and others}, |
|
534 title = {The {Haskell} 98 Language and Libraries: The Revised Report}, |
|
535 journal = {Journal of Functional Programming}, |
|
536 volume = 13, |
|
537 number = 1, |
|
538 pages = {0--255}, |
|
539 month = {Jan}, |
|
540 year = 2003, |
|
541 note = {\url{http://www.haskell.org/definition/}}} |
|
542 |
518 %K |
543 %K |
519 |
544 |
520 @InProceedings{kammueller-locales, |
545 @InProceedings{kammueller-locales, |
521 author = {Florian Kamm{\"u}ller and Markus Wenzel and |
546 author = {Florian Kamm{\"u}ller and Markus Wenzel and |
522 Lawrence C. Paulson}, |
547 Lawrence C. Paulson}, |
543 title = {Set Theory: An Introduction to Independence Proofs}, |
568 title = {Set Theory: An Introduction to Independence Proofs}, |
544 publisher = NH, |
569 publisher = NH, |
545 year = 1980} |
570 year = 1980} |
546 |
571 |
547 %L |
572 %L |
|
573 |
|
574 @manual{OCaml, |
|
575 author = {Xavier Leroy and others}, |
|
576 title = {The Objective Caml system -- Documentation and user's manual}, |
|
577 note = {\url{http://caml.inria.fr/pub/docs/manual-ocaml/}}} |
548 |
578 |
549 @InProceedings{lowe-fdr, |
579 @InProceedings{lowe-fdr, |
550 author = {Gavin Lowe}, |
580 author = {Gavin Lowe}, |
551 title = {Breaking and Fixing the {Needham}-{Schroeder} Public-Key |
581 title = {Breaking and Fixing the {Needham}-{Schroeder} Public-Key |
552 Protocol using {CSP} and {FDR}}, |
582 Protocol using {CSP} and {FDR}}, |
556 series = {LNCS 1055}, |
586 series = {LNCS 1055}, |
557 year = 1996, |
587 year = 1996, |
558 publisher = {Springer}, |
588 publisher = {Springer}, |
559 pages = {147-166}} |
589 pages = {147-166}} |
560 |
590 |
561 |
|
562 %M |
591 %M |
563 |
592 |
564 @Article{mw81, |
593 @Article{mw81, |
565 author = {Zohar Manna and Richard Waldinger}, |
594 author = {Zohar Manna and Richard Waldinger}, |
566 title = {Deductive Synthesis of the Unification Algorithm}, |
595 title = {Deductive Synthesis of the Unification Algorithm}, |
853 author = {Lawrence C. Paulson}, |
882 author = {Lawrence C. Paulson}, |
854 title = {{Isabelle}'s Logics: {FOL} and {ZF}}, |
883 title = {{Isabelle}'s Logics: {FOL} and {ZF}}, |
855 institution = CUCL, |
884 institution = CUCL, |
856 note = {\url{http://isabelle.in.tum.de/doc/logics-ZF.pdf}}} |
885 note = {\url{http://isabelle.in.tum.de/doc/logics-ZF.pdf}}} |
857 |
886 |
858 @manual{isabelle-classes, |
|
859 author = {Florian Haftmann}, |
|
860 title = {Haskell-style type classes with {Isabelle}/{Isar}}, |
|
861 institution = TUM, |
|
862 note = {\url{http://isabelle.in.tum.de/doc/classes.pdf}}} |
|
863 |
|
864 @manual{isabelle-codegen, |
|
865 author = {Florian Haftmann}, |
|
866 title = {Code generation from Isabelle theories}, |
|
867 institution = TUM, |
|
868 note = {\url{http://isabelle.in.tum.de/doc/codegen.pdf}}} |
|
869 |
|
870 @article{paulson-found, |
887 @article{paulson-found, |
871 author = {Lawrence C. Paulson}, |
888 author = {Lawrence C. Paulson}, |
872 title = {The Foundation of a Generic Theorem Prover}, |
889 title = {The Foundation of a Generic Theorem Prover}, |
873 journal = JAR, |
890 journal = JAR, |
874 volume = 5, |
891 volume = 5, |