{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,24]],"date-time":"2025-05-24T07:26:42Z","timestamp":1748071602136},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540649878"},{"type":"electronic","value":"9783540498018"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0055133","type":"book-chapter","created":{"date-parts":[[2006,7,27]],"date-time":"2006-07-27T05:09:13Z","timestamp":1153976953000},"page":"123-142","source":"Crossref","is-referenced-by-count":14,"title":["A comparison of PVS and Isabelle\/HOL"],"prefix":"10.1007","author":[{"given":"David","family":"Griffioen","sequence":"first","affiliation":[]},{"given":"Marieke","family":"Huisman","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,5,27]]},"reference":[{"key":"8_CR1","volume-title":"LNCS","author":"S. Agerholm","year":"1995","unstructured":"Sten Agerholm and Mike Gordon. Experiments with ZF set theory in HOL and Isabelle. In E. Thomas Schubert, Philip J. Windley, and James Alves-Foss, editors, Proceedings of the 8th International Workshop on Higher Order Logic Theorem Proving and Its Applications, Aspen Grove, UT, USA, volume 971 of LNCS. Springer-Verlag, September 1995."},{"key":"8_CR2","volume-title":"LNCS","author":"A. Ayari","year":"1996","unstructured":"Abdelwaheb Ayari and David A. Basin. Generic system support for deductive program development. In T. Margaria and B. Steffen, editors, Proceedings of the Workshop on Tools and Algorithms for the Construction and Analysis of Systems, Passau, Germany, volume 1055 of LNCS. Springer-Verlag, April 1996."},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"David Basin and Matt Kaufmann. The Boyer-Moore prover and Nuprl: An experimental compaxison. In G\u00e9rard Huet and Gordon Plotkin, editors, Logical Frameworks, pages 90\u2013119. Cambridge University Press, 1991.","DOI":"10.1017\/CBO9780511569807.006"},{"key":"8_CR4","unstructured":"Victor A. Carre\u00f1o and Paul S. Miner. Specification of the IEEE-854 floating-point standard in HOL and PVS. In HOL95: Eighth International Workshop on Higher-Order Logic Theorem Proving and Its Applications, Aspen Grove, UT, September 1995. Category B proceedings, available at http:\/\/lal.cs.byu.edu\/lal\/hol95\/Bprocs\/indexB.html."},{"key":"8_CR5","first-page":"40","volume-title":"Formalizing Space Shuttle software requirements","author":"J. Crow","year":"1996","unstructured":"Judith Crow and Ben L. Di Vito. Formalizing Space Shuttle software requirements. In First Workshop on Formal Methods in Software Practice (FMSP '96), pages 40\u201348, San Diego, CA, January 1996. Association for Computing Machinery."},{"key":"8_CR6","unstructured":"Judy Crow, Sam Owre, John Rushby, Natarajan Shankar, and Mandayam Srivas. A tutorial introduction to PVS. Presented at WIFT '95: Workshop on Industrial-Strength Formal Specification Techniques, Boca Raton, Florida, April 1995. Available, with specification files, at http:\/\/www.csl.sri.com\/wift-tutorial.html."},{"key":"8_CR7","unstructured":"Database of existing mechanized reasoning systems. http:\/\/www-formal.stanford.edu\/clt\/ARS\/systems.html."},{"key":"8_CR8","unstructured":"Marco Devillers, David Griffioen, Judi Romijn, and Frits Vaandrager. Verification of a leader election protocol formal methods applied to IEEE 1394. Technical Report CSI-R9728, Computing Science Institute, Catholic University of Nijmegen, 1997."},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Michael J.C. Gordon, Robin Milner, and Cristopher P. Wadsworth. Edinburgh LCF: A Mechanised Logic of Computation, volume 78 of LNCS. Springer-Verlag, 1979.","DOI":"10.1007\/3-540-09724-4"},{"key":"8_CR10","unstructured":"Mike Gordon. Notes on PVS from a HOL perspective. Available at http:\/\/www.cl.cam.ac.uk\/users\/mjcg\/PVS.html, August 1995."},{"volume-title":"volume 1275 of LNCS","year":"1997","key":"8_CR11","unstructured":"Elsa L. Gunter and Amy Felty, editors. Proceedings of the 10th International Workshop on Theorem Proving in Higher Order Logics, Murray Hill, NJ, USA, volume 1275 of LNCS. Springer-Verlag, August 1997."},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"Ulrich Hensel, Marieke Huisman, Bart Jacobs, and Hendrik Tews. Reasoning about classes in object-oriented languages: Logical models and tools. In Proceedings of ESOP at ETAPS '98, LNCS. Springer-Verlag, 1998. To appear.","DOI":"10.1007\/BFb0053566"},{"key":"8_CR13","first-page":"153","volume-title":"Constructive mathematics and computer programming","author":"P. Martin-L\u00f6f","year":"1982","unstructured":"Per Martin-L\u00f6f. Constructive mathematics and computer programming. In Sixth International Congress for Logic, Methodology, and Philosophy of Science, pages 153\u2013175. North Holland, Amsterdam, 1982."},{"key":"8_CR14","series-title":"Eurographics Series","volume-title":"Evaluating the interfaces of three theorem proving assistants","author":"N. A. Merriam","year":"1996","unstructured":"Nicholas A. Merriam and Michael D. Harrison. Evaluating the interfaces of three theorem proving assistants. In F. Bodart and J. Vanderdonckt, editors, Proceedings of the 3rd International Eurographics Workshop on Design, Specification, and Verification of Interactive Systems, Eurographics Series, Namur, Belgium, June 1996. Springer-Verlag."},{"key":"8_CR15","unstructured":"Sam Owre. http:\/\/www.csl.sri.com\/htbin\/pvs\/pvs-bug-list."},{"key":"8_CR16","unstructured":"Lawrence C. Paulson. Isabelle: The next 700 theorem provers. In P. Odifreddi, editor, Logic and Computer Science, pages 361\u2013386. Academic Press, 1990."},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"Lawrence C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of LNCS. Springer-Verlag, 1994.","DOI":"10.1007\/BFb0030541"},{"key":"8_CR18","unstructured":"Frank Pfenning. Isabelle bibliography. http:\/\/www.cl.cam.ac.uk\/Research\/HVG\/Isabelle\/biblio.html."},{"key":"8_CR19","unstructured":"John Rushby. PVS bibliography, http:\/\/www.csl.sri.com\/pvs-bib.html."},{"key":"8_CR20","doi-asserted-by":"crossref","unstructured":"John Rushby, Sam Owre, and N. Shankar. Subtypes for specifications: Predicate subtyping in PVS. IEEE Transactions on Software Engineering, 24, 1998. To appear.","DOI":"10.1109\/32.713327"},{"key":"8_CR21","first-page":"257","volume-title":"volume 1166 of LNCS","author":"N. Shankar","year":"1996","unstructured":"N. Shankar. PVS: Combining specification, proof checking, and model checking. In Mandayam Srivas and Albert Camilleri, editors, Formal Methods in Computer-Aided Design (FMCAD '96), volume 1166 of LNCS, pages 257\u2013264, Palo Alto, CA, November 1996. Springer-Verlag."},{"key":"8_CR22","doi-asserted-by":"crossref","unstructured":"Philip Wadler and Stephen Blott. How to make ad-hoc polymorphism less ad hoc. In 16'th ACM Symposium on Principles of Programming Languages, Austin, Texas, January 1989.","DOI":"10.1145\/75277.75283"},{"key":"8_CR23","unstructured":"Markus Wenzel. Using axiomatic type classes in Isabelle, a tutorial, 1995. http:\/\/www4.Informatik.tu-muenchen.de\/~wenzelm\/papers.html."},{"key":"8_CR24","volume-title":"volume 1275 of LNCS","author":"M. Wenzel","year":"1997","unstructured":"Markus Wenzel. Type classes and overloading in higher-order logic. In Gunter and Felty [11]."},{"issue":"4","key":"8_CR25","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1109\/32.588536","volume":"23","author":"W. D. Young","year":"1997","unstructured":"William D. Young. Comparing verification systems: Interactive Consistency in ACL2. IEEE Transactions on Software Engineering, 23(4):214\u2013223, April 1997.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"8_CR26","volume-title":"volume 1275 of LNCS","author":"V. Zammit","year":"1997","unstructured":"Vincent Zammit. A comparative study of Coq and HOL. In Gunter and Felty [11]."}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0055133","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,20]],"date-time":"2019-04-20T04:34:35Z","timestamp":1555734875000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0055133"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540649878","9783540498018"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/bfb0055133","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}