{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:23:52Z","timestamp":1725488632784},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540664635"},{"type":"electronic","value":"9783540482567"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48256-3_2","type":"book-chapter","created":{"date-parts":[[2007,8,3]],"date-time":"2007-08-03T20:15:22Z","timestamp":1186172122000},"page":"5-18","source":"Crossref","is-referenced-by-count":0,"title":["Disjoint Sums over Type Classes in HOL"],"prefix":"10.1007","author":[{"given":"Norbert","family":"V\u00f6lker","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[1999,9,17]]},"reference":[{"key":"2_CR1","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1016\/0304-3975(86)90044-7","volume":"45","author":"J.-Y. Girard","year":"1986","unstructured":"J.-Y. Girard. The system F of variable types, fifteen years later. Theoretical Computer Science, 45:159\u2013192, 1986.","journal-title":"Theoretical Computer Science"},{"key":"2_CR2","series-title":"Lect Notes Comput Sci","first-page":"191","volume-title":"Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics (TPHOLs\u201997)","author":"M.J.C. Gordon","year":"1997","unstructured":"M.J.C. Gordon. Set Theory, Higher Order Logic or Both? In Gunter and Felty A. Felty, editors. Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics (TPHOLs\u201997), LNCS 1275. Springer-Verlag, 1997 [4], pages 191\u2013201."},{"key":"2_CR3","unstructured":"M.J.C. Gordon and T.F. Melham. Introduction to HOL. Cambridge University Press, 1993."},{"key":"2_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028381","volume-title":"Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics (TPHOLs\u201997)","author":"E. L. Gunter","year":"1997","unstructured":"E. L. Gunter and A. Felty, editors. Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics (TPHOLs\u201997), LNCS 1275. Springer-Verlag, 1997."},{"key":"2_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1007\/978-3-540-49676-2_13","volume-title":"ZUM\u201998: The Z Formal Specification Notation","author":"M.C. Henson","year":"1998","unstructured":"M.C. Henson and S. Reeves. A logic for the schema calculus. In J. P. Bowen, A. Fett, and M. G. Hinchey, editors, ZUM\u201998: The Z Formal Specification Notation, LNCS 1493, pages 172\u2013191. Springer-Verlag, 1998."},{"key":"2_CR6","unstructured":"S.P. Jones and J. Hughes, editors. HASKELL98: A Non-strict, Purely Functional Language, February 1999. On-line available via http:\/\/haskell.org\/ ."},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"J.P. Bowen and M.J.C. Gordon. Z and HOL. In J.P. Bowen and J.A. Hall, editors, Z User Workshop, Cambridge 1994, Workshops in Computing, pages 141\u2013167. Springer-Verlag, 1994.","DOI":"10.1007\/978-1-4471-3452-7_9"},{"key":"2_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1007\/BFb0105411","volume-title":"Theorem Proving in Higher Order Logics \u2014 9th International Conference","author":"K. T. Santen","year":"1996","unstructured":"Kolyang, T. Santen, and B. Wolff. A Structure Preserving Encoding of Z in Isabelle\/HOL. In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem Proving in Higher Order Logics \u2014 9th International Conference, LNCS 1125, pages 283\u2013298. Springer Verlag, 1996."},{"key":"2_CR9","unstructured":"L. Lamport and L.C. Paulson. Should your specification language be typed? Technical Report 425, Computer Laboratory, University of Cambridge, May 1997."},{"issue":"1","key":"2_CR10","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1016\/0890-5401(91)90062-7","volume":"90","author":"Z. Luo","year":"1991","unstructured":"Zhaohui Luo. A higher-order calculus and theory abstraction. Information and Computation, 90(1):107\u2013137, 1991.","journal-title":"Information and Computation"},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"L.C. Paulson. A fixedpoint approach to implementing (co)inductive definitions. In A. Bundy, editor, Automated Deduction \u2014 CADE-12, LNAI 814, pages 148\u2013161. Springer-Verlag, 1994.","DOI":"10.1007\/3-540-58156-1_11"},{"key":"2_CR12","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. LNCS 828. Springer-Verlag, 1994."},{"key":"2_CR13","unstructured":"F. Regensburger. HOLCF: Eine konservative Erweiterung von HOL um LCF. Dissertation an der Technischen Universit\u00e4t M\u00fcnchen, 1994."},{"key":"2_CR14","unstructured":"J.M. Spivey. Understanding Z: a specification language and its formal semantics. Cambridge Tracts in Theoretical Computer Science 3. Cambridge University Press, 1988."},{"key":"2_CR15","unstructured":"R. Turner. Sets, types and typechecking. Journal of Logic and Computation, To Appear."},{"key":"2_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/BFb0028402","volume-title":"Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics (TPHOLs\u201997)","author":"M. Wenzel","year":"1997","unstructured":"M. Wenzel. Type classes and overloading in higher-order logic. In Gunter and Felty A. Felty, editors. Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics (TPHOLs\u201997), LNCS 1275. Springer-Verlag, 1997 [4], pages 307\u2013322."}],"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_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T18:58:40Z","timestamp":1556737120000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48256-3_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540664635","9783540482567"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-48256-3_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1999]]}}}