{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:30:23Z","timestamp":1774837823607,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540664635","type":"print"},{"value":"9783540482567","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48256-3_3","type":"book-chapter","created":{"date-parts":[[2007,8,3]],"date-time":"2007-08-03T20:15:22Z","timestamp":1186172122000},"page":"19-36","source":"Crossref","is-referenced-by-count":41,"title":["Inductive Datatypes in HOL \u2014 Lessons Learned in Formal-Logic Engineering"],"prefix":"10.1007","author":[{"given":"Stefan","family":"Berghofer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Markus","family":"Wenzel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[1999,9,17]]},"reference":[{"key":"3_CR1","first-page":"39","volume-title":"Images of SMC Research","author":"H. P. Barendregt","year":"1996","unstructured":"H. P. Barendregt. The quest for correctness. In Images of SMC Research, pages 39\u201358. Stichting Mathematisch Centrum, Amsterdam, 1996."},{"key":"3_CR2","unstructured":"S. Berghofer. Definitorische Konstruktion induktiver Datentypen in Isabelle\/HOL (in German). Master\u2019s thesis, Technische Universit\u00e4t M\u00fcnchen, 1998."},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"A. Church. A formulation of the simple theory of types. Journal of Symbolic Logic, pages 56\u201368, 1940.","DOI":"10.2307\/2266170"},{"key":"3_CR4","unstructured":"C. Cornes, J. Courant, J.-C. Filli\u00e2tre, G. Huet, P. Manoury, and C. Mu\u00f1oz. The Coq Proof Assistant User\u2019s Guide, version 6.1. INRIA-Rocquencourt et CNRSENS Lyon, 1996."},{"key":"3_CR5","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_CR6","doi-asserted-by":"crossref","unstructured":"E. L. Gunter. Why we can\u2019t have SML style datatype declarations in HOL. In L. J. M. Claesen and M. J. C. Gordon, editors, Higher Order Logic Theorem Proving and Its Applications, volume A-20 of IFIP Transactions, pages 561\u2013568. North-Holland Press, 1992.","DOI":"10.1016\/B978-0-444-89880-7.50042-5"},{"key":"3_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/3-540-57826-9_131","volume-title":"Higher Order Logic Theorem Proving and Its Applications","author":"E. L. Gunter","year":"1994","unstructured":"E. L. Gunter. A broader class of trees for recursive type definitions for HOL. In J. Joyce and C. Seger, editors, Higher Order Logic Theorem Proving and Its Applications, volume 780 of LNCS, pages 141\u2013154. Springer, 1994."},{"key":"3_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/3-540-60275-5_66","volume-title":"Higher Order Logic Theorem Proving and Its Applications: Proceedings of the 8th International Workshop","author":"J. Harrison","year":"1995","unstructured":"J. Harrison. Inductive definitions: automation and application. In P. J. Windley, T. Schubert, and J. Alves-Foss, editors, Higher Order Logic Theorem Proving and Its Applications: Proceedings of the 8th International Workshop, volume 971 of LNCS, pages 200\u2013213, Aspen Grove, Utah, 1995. Springer."},{"key":"3_CR9","unstructured":"J. Harrison. HOL done right. Unpublished draft, 1996."},{"key":"3_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/BFb0026991","volume-title":"Category Theory and Computer Science","author":"U. Hensel","year":"1997","unstructured":"U. Hensel and B. Jacobs. Proof principles for datatypes with iterated recursion. In E. Moggi and G. Rosolini, editors, Category Theory and Computer Science, volume 1290 of LNCS, pages 220\u2013241. Springer, 1997."},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"F. Kamm\u00fcller and M. Wenzel. Locales \u2014 a sectioning concept for Isabelle. Technical Report 449, University of Cambridge, Computer Laboratory, October 1998.","DOI":"10.1007\/3-540-48256-3_11"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"T. F. Melham. Automating recursive type definitions in higher order logic. In G. Birtwistle and P. A. Subrahmanyam, editors, Current Trends in Hardware Verification and Automated Theorem Proving, pages 341\u2013386. Springer, 1989.","DOI":"10.1007\/978-1-4612-3658-0_9"},{"key":"3_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0055146","volume-title":"Theorem Proving in Higher Order Logics","author":"W. Naraschewski","year":"1998","unstructured":"W. Naraschewski and M. Wenzel. Object-oriented verification based on record subtyping in higher-order logic. In J. Grundy and M. Newey, editors, Theorem Proving in Higher Order Logics, volume 1479 of LNCS. Springer, 1998."},{"key":"3_CR14","volume-title":"Proc. 25th ACM Symp. Principles of Programming Languages","author":"T. Nipkow","year":"1998","unstructured":"T. Nipkow and D. von Oheimb. Javalight is type-safe \u2014 definitely. In Proc. 25th ACM Symp. Principles of Programming Languages. ACM Press, New York, 1998."},{"key":"3_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61474-5_91","volume-title":"Computer Aided Verification","author":"S. Owre","year":"1996","unstructured":"S. Owre, S. Rajan, J. M. Rushby, N. Shankar, and M. Srivas. PVS: combining specification, proof checking, and model checking. In R. Alur and T. A. Henzinger, editors, Computer Aided Verification, volume 1102 of LNCS. Springer, 1996."},{"key":"3_CR16","unstructured":"S. Owre and N. Shankar. Abstract datatypes in PVS. Technical Report CSL-93-9R, Computer Science Laboratory, SRI International, 1993."},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"L. C. Paulson. A fixed-point approach to implementing (co)inductive defonitions. In A. Bundy, editor, Proceedings of the 12th International Conference on Automated Deduction, volume 814 of LNAI, pages 148\u2013161, Nancy, France, 1994. Springer.","DOI":"10.1007\/3-540-58156-1_11"},{"key":"3_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A Generic Theorem Prover","author":"L. C. Paulson","year":"1994","unstructured":"L. C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of LNCS. Springer, 1994."},{"issue":"2","key":"3_CR19","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1093\/logcom\/7.2.175","volume":"7","author":"L. C. Paulson","year":"1997","unstructured":"L. C. Paulson. Mechanizing coinduction and corecursion in higher-order logic. Journal of Logic and Computation, 7(2):175\u2013204, 1997.","journal-title":"Journal of Logic and Computation"},{"key":"3_CR20","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of Mathematical Foundations of Programming Semantics","author":"F. Pfenning","year":"1990","unstructured":"F. Pfenning and C. Paulin-Mohring. Inductively defined types in the Calculus of Constructions. In Proceedings of Mathematical Foundations of Programming Semantics, volume 442 of LNCS. Springer, 1990."},{"key":"3_CR21","series-title":"Lect Notes Comput Sci","volume-title":"9th International Conference on Theorem Proving in Higher Order Logics, TPHOLs\u201996","author":"K. Slind","year":"1996","unstructured":"K. Slind. Function definition in higher order logic. In J. Wright, J. Grundy, and J. Harrison, editors, 9th International Conference on Theorem Proving in Higher Order Logics, TPHOLs\u201996, volume 1125 of LNCS. Springer, 1996."},{"key":"3_CR22","series-title":"Lect Notes Comput Sci","volume-title":"10th International Conference on Theorem Proving in Higher Order Logics, TPHOLs\u201997","author":"K. Slind","year":"1997","unstructured":"K. Slind. Derivation and use of induction schemes in higher-order logic. In 10th International Conference on Theorem Proving in Higher Order Logics, TPHOLs\u201997, volume 1275 of LNCS. Springer, 1997."},{"key":"3_CR23","unstructured":"[23] N. V\u00f6lker. On the representation of datatypes in Isabelle\/HOL. In L. C. Paulson, editor, First Isabelle Users Workshop, 1995."},{"key":"3_CR24","series-title":"Lect Notes Comput Sci","volume-title":"10th International Conference on Theorem Proving in Higher Order Logics, TPHOLs\u201997","author":"2. M. Wenzel","year":"1997","unstructured":"[24] M. Wenzel. Type classes and overloading in higher-order logic. In 10th International Conference on Theorem Proving in Higher Order Logics, TPHOLs\u201997, volume 1275 of LNCS. Springer, 1997."}],"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\/3-540-48256-3_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T18:58:33Z","timestamp":1556737113000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48256-3_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540664635","9783540482567"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-48256-3_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1999]]}}}