{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:48:24Z","timestamp":1725490104531},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540745907"},{"type":"electronic","value":"9783540745914"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-74591-4_25","type":"book-chapter","created":{"date-parts":[[2007,8,22]],"date-time":"2007-08-22T14:49:52Z","timestamp":1187794192000},"page":"334-351","source":"Crossref","is-referenced-by-count":5,"title":["HOL2P - A System of Classical Higher Order Logic with Second Order Polymorphism"],"prefix":"10.1007","author":[{"given":"Norbert","family":"V\u00f6lker","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"25_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/10704973_2","volume-title":"Advanced Functional Programming","author":"R. Backhouse","year":"1999","unstructured":"Backhouse, R., Jansson, P., Jeuring, J., Meertens, L.: Generic programming - an introduction. In: Swierstra, S.D., Oliveira, J.N. (eds.) AFP 1998. LNCS, vol.\u00a01608, Springer, Heidelberg (1999)"},{"key":"25_CR2","volume-title":"Algebra of Programming","author":"R.S. Bird","year":"1997","unstructured":"Bird, R.S., de Moor, O.: Algebra of Programming. Prentice-Hall, Englewood Cliffs (1997)"},{"key":"25_CR3","first-page":"555","volume-title":"Proceedings 9th Int. Congress of Logic, Methodology and Philosophy of Science","author":"T. Coquand","year":"1994","unstructured":"Coquand, T.: A new paradox in type theory. In: Prawitz, D., Skyrms, B., Westerst\u00e5hl, D. (eds.) Proceedings 9th Int. Congress of Logic, Methodology and Philosophy of Science, pp. 555\u2013570. North-Holland, Amsterdam (1994)"},{"key":"25_CR4","series-title":"Cambridge Tracts in Theoretical Computer Science","volume-title":"Proofs and Types","author":"J.-Y. Girard","year":"1989","unstructured":"Girard, J.-Y., Lafont, Y., Taylor, P.: Proofs and Types. Cambridge Tracts in Theoretical Computer Science, vol.\u00a07. Cambridge University Press, Cambridge (1989)"},{"key":"25_CR5","unstructured":"Glimming, J.: Logic and Automation for Algebra of Programming. PhD thesis, MSc Thesis, University of Oxford (2001)"},{"key":"25_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF","author":"M. Gordon","year":"1979","unstructured":"Gordon, M., Wadsworth, C.P., Milner, R.: Edinburgh LCF. LNCS, vol.\u00a078. Springer, Heidelberg (1979)"},{"key":"25_CR7","volume-title":"Introduction to HOL","author":"M.J.C. Gordon","year":"1993","unstructured":"Gordon, M.J.C., Melham, T.F.: Introduction to HOL. Cambridge University Press, Cambridge (1993)"},{"key":"25_CR8","series-title":"Real-Time Safety Critical Systems Series","volume-title":"Towards Verified Systems","author":"M.J.C. Gordon","year":"1994","unstructured":"Gordon, M.J.C., Pitts, A.: The HOL Logic and System. In: Bowen, J. (ed.) Towards Verified Systems. Real-Time Safety Critical Systems Series, vol.\u00a02, Elsevier, Amsterdam (1994)"},{"key":"25_CR9","unstructured":"Harrison, J.: The HOL Light System Reference \u2013 Version 2.20 (2006), \n                  \n                    http:\/\/www.cl.cam.ac.uk\/~jrh13\/hol-light"},{"key":"25_CR10","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","DOI":"10.1007\/11814771_17","volume-title":"Automated Reasoning","author":"J. Harrison","year":"2006","unstructured":"Harrison, J.: Towards self-verification in HOL-Light. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, Springer, Heidelberg (2006)"},{"key":"25_CR11","doi-asserted-by":"crossref","unstructured":"Hu, Z., Iwasaki, H., Takeichi, M.: Deriving structural hylomorphisms from recursive definitions. In: ICFP, pp. 73\u201382 (1996)","DOI":"10.1145\/232627.232637"},{"key":"25_CR12","doi-asserted-by":"crossref","unstructured":"Jones, S.P., Vytiniotis, D., Weirich, S., Shields, M.: Practical type inference for arbitrary-rank types. Journal of Functional Programming\u00a017(1) (2007)","DOI":"10.1017\/S0956796806006034"},{"key":"25_CR13","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-9839-7","volume-title":"Categories for the Working Mathematician","author":"S. Mac Lane","year":"1971","unstructured":"Mac Lane, S.: Categories for the Working Mathematician. Springer, Heidelberg (1971)"},{"issue":"1\u20132","key":"25_CR14","first-page":"7","volume":"3","author":"T.F. Melham","year":"1994","unstructured":"Melham, T.F.: The HOL logic extended with quantification over type variables. Formal Methods in System Design\u00a03(1\u20132), 7\u201324 (1994)","journal-title":"Formal Methods in System Design"},{"key":"25_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"25_CR16","volume-title":"Types and Programming Languages","author":"B.C. Pierce","year":"2002","unstructured":"Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)"},{"key":"25_CR17","unstructured":"The Coq Development Team. The Coq Proof Assistant Reference Manual \u2013 Version V8.0 (2004), \n                  \n                    http:\/\/coq.inria.fr"},{"key":"25_CR18","unstructured":"V\u00f6lker, N.: HOL2P Prototype Implementation (2007), \n                  \n                    http:\/\/cswww.essex.ac.uk\/staff\/norbert\/hol2p"},{"issue":"9","key":"25_CR19","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1145\/1160074.1159838","volume":"41","author":"D. Vytiniotis","year":"2006","unstructured":"Vytiniotis, D., Weirich, S., Jones, S.P.: Boxy types: inference for higher-rank types and impredicativity. ACM SIGPLAN Notices\u00a041(9), 251\u2013262 (2006)","journal-title":"ACM SIGPLAN Notices"},{"key":"25_CR20","volume-title":"Functional Programming Languages and Computer Architecture","author":"P. Wadler","year":"1989","unstructured":"Wadler, P.: Theorems for free? In: Functional Programming Languages and Computer Architecture, Springer, Heidelberg (1989)"},{"key":"25_CR21","doi-asserted-by":"crossref","unstructured":"Wadler, P.: The essence of functional programming. In: POPL, pp. 1\u201314 (1992)","DOI":"10.1145\/143165.143169"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-74591-4_25.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:28:10Z","timestamp":1619519290000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74591-4_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540745907","9783540745914"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74591-4_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}