{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:22:04Z","timestamp":1725664924530},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540602750"},{"type":"electronic","value":"9783540447849"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60275-5_55","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T18:06:20Z","timestamp":1330279580000},"page":"32-45","source":"Crossref","is-referenced-by-count":8,"title":["Experiments with ZF set theory in HOL and Isabelle"],"prefix":"10.1007","author":[{"given":"Sten","family":"Agerholm","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mike","family":"Gordon","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"3_CR1","unstructured":"S. Agerholm. Formalising a model of the \u03bb-calculus in HOL-ST. Technical Report 354, University of Cambridge Computer Laboratory, November 1994."},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"S. Agerholm. A HOL Basis for Reasoning about Functional Programs. PhD thesis, BRICS, Department of Computer Science, University of Aarhus, December 1994. Available as Technical Report RS-94-44.","DOI":"10.7146\/brics.v1i44.21598"},{"key":"3_CR3","unstructured":"S. Agerholm. A comparison of HOL-ST and Isabelle\/ZF. Technical Report 369, University of Cambridge Computer Laboratory, 1995."},{"volume-title":"Computable Set Theory, volume 1","year":"1989","key":"3_CR4","unstructured":"D. Cantone, A. Ferro, and E. Omodeo, editors. Computable Set Theory, volume 1. Clarendon Press, Oxford, 1989."},{"key":"3_CR5","unstructured":"R. L. Constable et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, 1986."},{"key":"3_CR6","unstructured":"F. Corella. Mechanizing set theory. Technical Report 232, University of Cambridge Computer Laboratory, 1991."},{"key":"3_CR7","unstructured":"G. Dowek, A. Felty, H. Herbelin, G. Huet, C. Murthy, C. Parent, C. Paulin-Mohring, and B. Werner. The Coq proof assistant user's guide \u2014 version 5.8. Technical Report 154, INRIA-Rocquencourt, 1993."},{"key":"3_CR8","unstructured":"Roman Matuszewski (ed). Formalized Mathematics. Universit\u00e9 Catholique de Louvain, 1990-. Subscription is $10 per issue or $50 per year (including postage). Subscriptions and orders should be addressed to: Fondation Philippe le Hodey, MIZAR, Av.F.Roosevelt 35, 1050 Brussels, Belgium (fax: +32 (2) 640.89.68)."},{"issue":"2","key":"3_CR9","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/BF00881906","volume":"11","author":"W. M. Farmer","year":"1993","unstructured":"W. M. Farmer, J. D. Guttman, and F. Javier Thayer. IMPS: An interactive mathematical proof system. Journal of Automated Reasoning, 11(2):213\u2013248, 1993.","journal-title":"Journal of Automated Reasoning"},{"key":"3_CR10","unstructured":"S. Finn and M. P. Fourman. L2 \u2014 The LAMBDA Logic. Abstract Hardware Limited, September 1993. In LAMBDA 4.3 Reference Manuals."},{"key":"3_CR11","unstructured":"M. J. C. Gordon. Merging HOL with set theory: preliminary experiments. Technical Report 353, University of Cambridge Computer Laboratory, 1994."},{"key":"3_CR12","unstructured":"M. J. C. Gordon and T. F. Melham, editors. Introduction to HOL: A Theorem-proving Environment for Higher-Order Logic. Cambridge University Press, 1993."},{"key":"3_CR13","unstructured":"F. K. Hanna, N. Daeche, and M. Longley. Veritas+: a specification language based on type theory. In M. Leeser and G. Brown, editors, Hardware specification, verification and synthesis: mathematical aspects, volume 408 of Lecture Notes in Computer Science, pages 358\u2013379. Springer-Verlag, 1989."},{"key":"3_CR14","unstructured":"C. B. Jones. Systematic Software Development using VDM. Prentice Hall International, 1990."},{"key":"3_CR15","unstructured":"L. Lamport. TLA+. Available on the World Wide Web at the URL: http:\/\/www.research.digital.com\/SRC\/tla\/tla.html."},{"key":"3_CR16","volume-title":"Technical Report ECS-LFCS-92-211","author":"Z. Luo","year":"1992","unstructured":"Z. Luo and R. Pollack. LEGO proof development system: User's manual. Technical Report ECS-LFCS-92-211, University of Edinburgh, LFCS, Computer Science Department, University of Edinburgh, The King's Buildings, Edinburgh, EH9 3JZ, May 1992."},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"L. Magnusson and B. Nordstr\u00f6m. The ALF proof editor and its proof engine. In Types for Proofs and Programs: International Workshop TYPES '93, number 806 in Lecture Notes in Computer Science, pages 213\u2013237. Springer-Verlag, 1994.","DOI":"10.1007\/3-540-58085-9_78"},{"key":"3_CR18","unstructured":"D. A. McAllester. ONTIC: A Knowledge Representation System for Mathematics. MIT Press, 1989."},{"key":"3_CR19","doi-asserted-by":"crossref","unstructured":"P. M. Melliar-Smith and John Rushby. The enhanced HDM system for specification and verification. In Proc. Verkshop III, volume 10 of ACM Software Engineering Notes, pages 41\u201343. Springer-Verlag, 1985.","DOI":"10.1145\/1012497.1012511"},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"L. C. Paulson. Logic and Computation: Interactive Proof with Cambridge LCF. Cambridge Tracts in Theoretical Computing 2, Cambridge University Press, 1987.","DOI":"10.1017\/CBO9780511526602"},{"issue":"3","key":"3_CR21","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1007\/BF00881873","volume":"11","author":"L. C. Paulson","year":"1993","unstructured":"L. C. Paulson. Set theory for verification: I. From foundations to functions. Journal of Automated Reasoning, 11(3):353\u2013389, 1993.","journal-title":"Journal of Automated Reasoning"},{"key":"3_CR22","unstructured":"L. C. Paulson. Set theory for verification: II. Induction and Recursion. Technical Report 312, University of Cambridge Computer Laboratory, 1993."},{"key":"3_CR23","doi-asserted-by":"crossref","unstructured":"L. C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of Lecture Notes in Computer Science. Springer-Verlag, 1994.","DOI":"10.1007\/BFb0030541"},{"key":"3_CR24","doi-asserted-by":"crossref","unstructured":"K. D. Petersen. Graph model of lambda in higher order logic. In J. J. Joyce and C. H. Seger, editors, Proceedings of the 6th International Workshop on Higher Order Logic Theorem Proving and its Applications, volume 780 of Lecture Notes in Computer Science. Springer-Verlag, 1994.","DOI":"10.1007\/3-540-57826-9_122"},{"key":"3_CR25","unstructured":"G. Plotkin. Domains. Course notes, Department of Computer Science, University of Edinburgh, 1983."},{"key":"3_CR26","unstructured":"PVS World Wide Web page. http:\/\/www.csl.sri.com\/pvs\/overview.html."},{"key":"3_CR27","unstructured":"Piotr Rudnicki. An Overview of the MIZAR Project. Unpublished; but available by anonymous FTP from menaik.cs.ualberta.ca in the directory pub\/Mizar\/Mizar_Over.tar.Z, 1992."},{"key":"3_CR28","volume-title":"Technical Report TR-91-5449-02","author":"M. Saaltink","year":"1991","unstructured":"M. Saaltink. Z and EVES. Technical Report TR-91-5449-02, Odyssey Research Associates, 265 Carling Avenue, Suite 506, Ottawa, Ontario K1S 2E1, Canada, October 1991."},{"key":"3_CR29","doi-asserted-by":"crossref","unstructured":"M. Smyth and G. D. Plotkin. The category-theoretic solution of recursive domain equations. SIAM Journal of Computing, 11, 1982.","DOI":"10.1137\/0211062"},{"key":"3_CR30","unstructured":"J. M. Spivey. The Z Notation: A Reference Manual. Prentice Hall International Series in Computer Science, 2nd edition, 1992."}],"container-title":["Lecture Notes in Computer Science","Higher Order Logic Theorem Proving and Its Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60275-5_55.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:57:16Z","timestamp":1605646636000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60275-5_55"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540602750","9783540447849"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/3-540-60275-5_55","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}