599 volume = 11, |
599 volume = 11, |
600 number = 2, |
600 number = 2, |
601 year = 1993, |
601 year = 1993, |
602 pages = {213-248}} |
602 pages = {213-248}} |
603 |
603 |
|
604 @article{Farmer:2008, |
|
605 author = {William M. Farmer}, |
|
606 title = {The seven virtues of simple type theory}, |
|
607 journal = {J. Applied Logic}, |
|
608 volume = {6}, |
|
609 number = {3}, |
|
610 pages = {267--286}, |
|
611 year = {2008}, |
|
612 url = {http://dx.doi.org/10.1016/j.jal.2007.11.001}, |
|
613 } |
|
614 |
604 @InProceedings{felty91a, |
615 @InProceedings{felty91a, |
605 Author = {Amy Felty}, |
616 Author = {Amy Felty}, |
606 Title = {A Logic Program for Transforming Sequent Proofs to Natural |
617 Title = {A Logic Program for Transforming Sequent Proofs to Natural |
607 Deduction Proofs}, |
618 Deduction Proofs}, |
608 crossref = {extensions91}, |
619 crossref = {extensions91}, |
676 author = {Jean-Yves Girard}, |
687 author = {Jean-Yves Girard}, |
677 title = {Proofs and Types}, |
688 title = {Proofs and Types}, |
678 year = 1989, |
689 year = 1989, |
679 publisher = CUP, |
690 publisher = CUP, |
680 note = {Translated by Yves Lafont and Paul Taylor}} |
691 note = {Translated by Yves Lafont and Paul Taylor}} |
|
692 |
|
693 @TechReport{Gordon:1985:HOL, |
|
694 author = {M. J. C. Gordon}, |
|
695 title = {{HOL}: A machine oriented formulation of higher order logic}, |
|
696 institution = {University of Cambridge Computer Laboratory}, |
|
697 year = 1985, |
|
698 number = 68 |
|
699 } |
681 |
700 |
682 @Book{mgordon-hol, |
701 @Book{mgordon-hol, |
683 editor = {M. J. C. Gordon and T. F. Melham}, |
702 editor = {M. J. C. Gordon and T. F. Melham}, |
684 title = {Introduction to {HOL}: A Theorem Proving Environment for Higher Order Logic}, |
703 title = {Introduction to {HOL}: A Theorem Proving Environment for Higher Order Logic}, |
685 publisher = CUP, |
704 publisher = CUP, |
974 @manual{isabelle-function, |
993 @manual{isabelle-function, |
975 author = {Alexander Krauss}, |
994 author = {Alexander Krauss}, |
976 title = {Defining Recursive Functions in {Isabelle/HOL}}, |
995 title = {Defining Recursive Functions in {Isabelle/HOL}}, |
977 institution = TUM, |
996 institution = TUM, |
978 note = {\url{http://isabelle.in.tum.de/doc/functions.pdf}} |
997 note = {\url{http://isabelle.in.tum.de/doc/functions.pdf}} |
|
998 } |
|
999 |
|
1000 @inproceedings{Kuncar-Popescu:2015, |
|
1001 author = {Ondrej Kuncar and Andrei Popescu}, |
|
1002 title = {A Consistent Foundation for {Isabelle/HOL}}, |
|
1003 editor = {Christian Urban and Xingyuan Zhang}, |
|
1004 booktitle = {Interactive Theorem Proving - 6th International Conference, {ITP} |
|
1005 2015, Nanjing, China, August 24-27, 2015, Proceedings}, |
|
1006 year = {2015}, |
|
1007 url = {http://dx.doi.org/10.1007/978-3-319-22102-1_16}, |
|
1008 series = {Lecture Notes in Computer Science}, |
|
1009 volume = {9236}, |
|
1010 publisher = {Springer}, |
|
1011 year = {2015}, |
979 } |
1012 } |
980 |
1013 |
981 @Book{kunen80, |
1014 @Book{kunen80, |
982 author = {Kenneth Kunen}, |
1015 author = {Kenneth Kunen}, |
983 title = {Set Theory: An Introduction to Independence Proofs}, |
1016 title = {Set Theory: An Introduction to Independence Proofs}, |