145 and Jan Smith}, |
145 and Jan Smith}, |
146 series = {LNCS}, |
146 series = {LNCS}, |
147 year = 2000 |
147 year = 2000 |
148 } |
148 } |
149 |
149 |
|
150 @InProceedings{Bauer-Wenzel:2001, |
|
151 author = {Gertrud Bauer and Markus Wenzel}, |
|
152 title = {Calculational reasoning revisited --- an {Isabelle/Isar} experience}, |
|
153 crossref = {tphols2001}} |
|
154 |
150 @INPROCEEDINGS{Berghofer-Nipkow:2000:TPHOL, |
155 @INPROCEEDINGS{Berghofer-Nipkow:2000:TPHOL, |
151 crossref = "tphols2000", |
156 crossref = "tphols2000", |
152 title = "Proof terms for simply typed higher order logic", |
157 title = "Proof terms for simply typed higher order logic", |
153 author = "Stefan Berghofer and Tobias Nipkow", |
158 author = "Stefan Berghofer and Tobias Nipkow", |
154 pages = "38--52"} |
159 pages = "38--52"} |
862 title = {Isabelle: A Generic Theorem Prover}, |
867 title = {Isabelle: A Generic Theorem Prover}, |
863 publisher = {Springer}, |
868 publisher = {Springer}, |
864 year = 1994, |
869 year = 1994, |
865 note = {LNCS 828}} |
870 note = {LNCS 828}} |
866 |
871 |
|
872 @Book{isabelle-hol-book, |
|
873 author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel}, |
|
874 title = {Isabelle/HOL --- A Proof Assistant for Higher-Order Logic}, |
|
875 publisher = {Springer}, |
|
876 year = 2002, |
|
877 note = {LNCS 2283}} |
|
878 |
867 @InCollection{paulson-markt, |
879 @InCollection{paulson-markt, |
868 author = {Lawrence C. Paulson}, |
880 author = {Lawrence C. Paulson}, |
869 title = {Tool Support for Logics of Programs}, |
881 title = {Tool Support for Logics of Programs}, |
870 booktitle = {Mathematical Methods in Program Development: |
882 booktitle = {Mathematical Methods in Program Development: |
871 Summer School Marktoberdorf 1996}, |
883 Summer School Marktoberdorf 1996}, |
1384 editor = {Bertot, Y. and Dowek, G. and Hirschowitz, A. and |
1396 editor = {Bertot, Y. and Dowek, G. and Hirschowitz, A. and |
1385 Paulin, C. and Thery, L.}, |
1397 Paulin, C. and Thery, L.}, |
1386 series = {LNCS 1690}, |
1398 series = {LNCS 1690}, |
1387 year = 1999} |
1399 year = 1999} |
1388 |
1400 |
1389 @PROCEEDINGS{tphols2000, |
1401 @Proceedings{tphols2000, |
1390 editor = "J. Harrison and M. Aagaard", |
1402 title = {Theorem Proving in Higher Order Logics: {TPHOLs} 2000}, |
1391 booktitle = "Theorem Proving in Higher Order Logics: |
1403 booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} 2000}, |
1392 13th International Conference, TPHOLs 2000", |
1404 editor = {J. Harrison and M. Aagaard}, |
1393 series = "Lecture Notes in Computer Science", |
1405 series = {LNCS 1869}, |
1394 volume = 1869, |
1406 year = 2000} |
1395 year = 2000, |
1407 |
1396 publisher = "Springer-Verlag"} |
1408 @Proceedings{tphols2001, |
|
1409 title = {Theorem Proving in Higher Order Logics: {TPHOLs} 2001}, |
|
1410 booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} 2001}, |
|
1411 editor = {R. J. Boulton and P. B. Jackson}, |
|
1412 series = {LNCS 2152}, |
|
1413 year = 2001} |