{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,18]],"date-time":"2026-04-18T23:04:53Z","timestamp":1776553493453,"version":"3.51.2"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540615873","type":"print"},{"value":"9783540706410","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/bfb0105405","type":"book-chapter","created":{"date-parts":[[2011,11,9]],"date-time":"2011-11-09T16:17:00Z","timestamp":1320855420000},"page":"191-201","source":"Crossref","is-referenced-by-count":17,"title":["Set theory, higher order logic or both?"],"prefix":"10.1007","author":[{"given":"Mike","family":"Gordon","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2007,4,29]]},"reference":[{"key":"13_CR1","unstructured":"S. Agerholm. Formalising a model of the \u03bb-calculus in HOL-ST. Technical Report 354, University of Cambridge Computer Laboratory, 1994."},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"S. Agerholm and M.J.C. Gordon. Experiments with ZF Set Theory in HOL and Isabelle. In E. T. Schubert, P. J. Windley, and J. Alves-Foss, editors, Higher Order Logic Theorem Proving and Its Applications: 8th International Workshop, volume 971 of Lecture Notes in Computer Science, pages 32\u201345. Springer-Verlag, September 1995.","DOI":"10.1007\/3-540-60275-5_55"},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"Jackson Paul B. Exploring abstract algebra in constructive type theory. In A. Bundy, editor, 12th Conference on Automated Deduction, Lecture Notes in Artifical Intelligence. Springer, June 1994.","DOI":"10.1007\/3-540-58156-1_43"},{"key":"13_CR4","unstructured":"R. J. Boulton, A. D. Gordon, M. J. C. Gordon, J. R. Harrison, J. M. J. Herbert, and J. Van Tassel. Experience with embedding hardware description languages in HOL. In V. Stavridou, T. F. Melham, and R. T. Boute, editors, Theorem Provers in Circuit Design: Theory, Practice and Experience: Proceedings of the IFIP TC10\/WG 10.2 International Conference, IFIP Transactions A-10, pages 129\u2013156. North-Holland, June 1992."},{"key":"13_CR5","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"A. Church. A formulation of the simple theory of types. The Journal of Symbolic Logic, 5:56\u201368, 1940.","journal-title":"The Journal of Symbolic Logic"},{"key":"13_CR6","unstructured":"R. L. Constable et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, 1986."},{"key":"13_CR7","unstructured":"Thierry Coquand. An analysis of Girard's paradox. In Proceedings, Symposium on Logic in Computer Science, pages 227\u2013236, Cambridge, Massachusetts, 16\u201318 June 1986. IEEE Computer Society."},{"key":"13_CR8","unstructured":"Francisco Corella. Mechanizing set theory. Technical Report 232, University of Cambridge Computer Laboratory, August 1991."},{"key":"13_CR9","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."},{"issue":"2","key":"13_CR10","doi-asserted-by":"publisher","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":"13_CR11","unstructured":"S. Finn and M. P. Fourman. L2 \u2014 The LAMBDA Logic. Abstract Hardware Limited, September 1993. In LAMBDA 4.3 Reference Manuals."},{"key":"13_CR12","unstructured":"M. J. C. Gordon. Merging HOL with set theory. Technical Report 353, University of Cambridge Computer Laboratory, November 1994."},{"key":"13_CR13","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":"13_CR14","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":"13_CR15","unstructured":"C. B. Jones. Systematic Software Development using VDM. Prentice Hall International, 1990."},{"key":"13_CR16","doi-asserted-by":"crossref","unstructured":"L. Lamport and S. Merz. Specifying and verifying fault-tolerant systems. In Proceedings of FTRTFT'94, Lecture Notes in Computer Science. Springer-Verlag, 1994. See also: http:\/\/www.research.digital.com\/SRC\/tla\/papers.html#TLA+.","DOI":"10.1007\/3-540-58468-4_159"},{"key":"13_CR17","series-title":"Technical Report","volume-title":"LEGO proof development system: User's manual","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":"13_CR18","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\u2019 93, pages 213\u2013237. Springer, published 1994. LNCS 806.","DOI":"10.1007\/3-540-58085-9_78"},{"key":"13_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":"13_CR20","unstructured":"R. P. Nederpelt, J. H. Geuvers, and R. C. De Vrijer, editors. Selected Papers on Automath, volume 133 of Studies in Logic and The Foundations of Mathematics. North Holland, 1994."},{"key":"13_CR21","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":"13_CR22","unstructured":"PVS Web page. http:\/\/www.csl.sri.com\/pvs\/overview.html."},{"key":"13_CR23","unstructured":"Piotr Rudnicki. An Overview of the MIZAR Project. Unpublished manuscript; but available by anonymous FTP from menaik.cs.ualberta.ca in the directory pub\/Mizar\/Mizar_Over.tar.Z, 1992."},{"key":"13_CR24","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","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0105405","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,19]],"date-time":"2019-06-19T05:44:37Z","timestamp":1560923077000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0105405"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540615873","9783540706410"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/bfb0105405","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996]]}}}