{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T21:18:48Z","timestamp":1725743928906},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642404467"},{"type":"electronic","value":"9783642404474"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-40447-4_8","type":"book-chapter","created":{"date-parts":[[2013,8,6]],"date-time":"2013-08-06T01:00:39Z","timestamp":1375750839000},"page":"117-132","source":"Crossref","is-referenced-by-count":1,"title":["The Design of a Practical Proof Checker for a Lazy Functional Language"],"prefix":"10.1007","author":[{"given":"Adam","family":"Procter","sequence":"first","affiliation":[]},{"given":"William L.","family":"Harrison","sequence":"additional","affiliation":[]},{"given":"Aaron","family":"Stump","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"8_CR1","unstructured":"The Coq development team: The Coq Proof Assistant Reference Manual. LogiCal Project, Version 8.3 (2010)"},{"key":"8_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/3-540-46028-4_4","volume-title":"Implementation of Functional Languages","author":"M. Mol de","year":"2002","unstructured":"de Mol, M., van Eekelen, M., Plasmeijer, R.: Theorem Proving for Functional Programmers. In: Arts, T., Mohnen, M. (eds.) IFL 2002. LNCS, vol.\u00a02312, pp. 55\u201371. Springer, Heidelberg (2002)"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"Gibbons, J., Hinze, R.: Just do it: Simple monadic equational reasoning. In: ICFP (September 2011)","DOI":"10.1145\/2034773.2034777"},{"key":"8_CR4","unstructured":"Peyton Jones, S. (ed.): Haskell 98 Language and Libraries, the Revised Report. Cambridge University Press (2003)"},{"key":"8_CR5","unstructured":"Gim\u00e9nez, C.E.: Un calcul de constructions infinies et son application a la verification de systemes communicants, Ph.D. thesis (1996)"},{"key":"8_CR6","unstructured":"Yorgey, B.: Typeclassopedia, http:\/\/www.haskell.org\/haskellwiki\/Typeclassopedia (accessed May 31, 2012)"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"Stump, A., Deters, M., Petcher, A., Schiller, T., Simpson, T.: Verified Programming in Guru. In: PLPV 2008 (2008)","DOI":"10.1145\/1481848.1481856"},{"key":"8_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/978-3-642-03359-9_10","volume-title":"Theorem Proving in Higher Order Logics","author":"N. Benton","year":"2009","unstructured":"Benton, N., Kennedy, A., Varming, C.: Some Domain Theory and Denotational Semantics in Coq. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 115\u2013130. Springer, Heidelberg (2009)"},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Nanevski, A., Morrisett, G., Shinnar, A., Govereau, P., Birkedal, L.: Ynot: Reasoning with the awkward squad. In: ICFP 2008 (2008)","DOI":"10.1145\/1411204.1411237"},{"issue":"5-6","key":"8_CR10","doi-asserted-by":"publisher","first-page":"865","DOI":"10.1017\/S0956796808006953","volume":"18","author":"A. Nanevski","year":"2008","unstructured":"Nanevski, A., Morrisett, G., Birkedal, L.: Hoare Type Theory, Polymorphism and Separation. J. Funct. Program.\u00a018(5-6), 865\u2013911 (2008)","journal-title":"J. Funct. Program."},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"van Kesteren, R., van Eekelen, M., de Mol, M.: Proof support for general type classes. In: TFP 2004, pp. 1\u201316 (2004)","DOI":"10.2307\/j.ctv36xw0k5.4"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/11964681_3","volume-title":"Implementation and Application of Functional Languages","author":"M. Eekelen van","year":"2006","unstructured":"van Eekelen, M., de Mol, M.: Proof tool support for explicit strictness. In: Butterfield, A., Grelck, C., Huch, F. (eds.) IFL 2005. LNCS, vol.\u00a04015, pp. 37\u201354. Springer, Heidelberg (2006)"},{"key":"8_CR13","doi-asserted-by":"crossref","unstructured":"Wadler, P., Blott, S.: How to make ad-hoc polymorphism less ad hoc. In: POPL 1989, pp. 60\u201376 (1989)","DOI":"10.1145\/75277.75283"},{"key":"8_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-3-540-71067-7_23","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Sozeau","year":"2008","unstructured":"Sozeau, M., Oury, N.: First-class type classes. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 278\u2013293. Springer, Heidelberg (2008)"},{"key":"8_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/11541868_10","volume-title":"Theorem Proving in Higher Order Logics","author":"B. Huffman","year":"2005","unstructured":"Huffman, B., Matthews, J., White, P.: Axiomatic constructor classes in Isabelle\/HOLCF. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 147\u2013162. Springer, Heidelberg (2005)"},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"Hallgren, T.: Haskell Tools from the Programatica Project. In: Haskell 2003, pp. 103\u2013106 (2003)","DOI":"10.1145\/871895.871907"},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"Xu, D.N.: Extended static checking for Haskell. In: Haskell 2006, pp. 48\u201359 (2006)","DOI":"10.1145\/1159842.1159849"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"Xu, D.N., Peyton Jones, S., Claessen, K.: Static contract checking for Haskell. In: POPL 2009, pp. 41\u201352 (2009)","DOI":"10.1145\/1594834.1480889"},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"Runciman, C., Naylor, M., Lindblad, F.: SmallCheck and Lazy SmallCheck: Automatic Exhaustive Testing for Small Values. In: Haskell 2008, pp. 37\u201348 (2008)","DOI":"10.1145\/1411286.1411292"},{"key":"8_CR20","doi-asserted-by":"crossref","unstructured":"Claessen, K., Hughes, J.: QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs. In: ICFP 2000, pp. 268\u2013279 (2000)","DOI":"10.1145\/357766.351266"},{"key":"8_CR21","doi-asserted-by":"crossref","unstructured":"Gill, A.: Introducing the Haskell Equational Reasoning Assistant. In: Haskell 2006, pp. 108\u2013109 (2006)","DOI":"10.1145\/1159842.1159856"},{"key":"8_CR22","doi-asserted-by":"publisher","first-page":"1217","DOI":"10.1016\/j.tcs.2008.11.020","volume":"410","author":"L. Schr\u00f6der","year":"2009","unstructured":"Schr\u00f6der, L., Mossakowski, T.: HasCasl: Integrated higher-order specification and program development. Theor. Comput. Sci.\u00a0410, 1217\u20131260 (2009)","journal-title":"Theor. Comput. Sci."},{"key":"8_CR23","unstructured":"Kieburtz, R.B.: P-logic: property verification for Haskell programs (2002)"},{"key":"8_CR24","doi-asserted-by":"publisher","first-page":"837","DOI":"10.1017\/S0956796805005666","volume":"15","author":"W.L. Harrison","year":"2005","unstructured":"Harrison, W.L., Kieburtz, R.B.: The Logic of Demand in Haskell. J. Funct. Program.\u00a015, 837\u2013891 (2005)","journal-title":"J. Funct. Program."},{"key":"8_CR25","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1145\/232627.232640","volume-title":"ICFP 1996: Proceedings of the First ACM SIGPLAN International Conference on Functional Programming","author":"B.T. Howard","year":"1996","unstructured":"Howard, B.T.: Inductive, coinductive, and pointed types. In: ICFP 1996: Proceedings of the First ACM SIGPLAN International Conference on Functional Programming, pp. 102\u2013109. ACM, New York (1996)"},{"key":"8_CR26","unstructured":"Casinghino III, C., Eades, H.D., Kimmell, G., Sjoberg, V., Sheard, T., Stump, A., Weirich, S.: The preliminary design of the Trellys core language Talk and discussion session at PLPV 2011 (2011)"},{"key":"8_CR27","unstructured":"Norell, U.: Towards a practical programming language based on dependent type theory. Department of Computer Science and Engineering, Chalmers University of Technology (September 2007)"}],"container-title":["Lecture Notes in Computer Science","Trends in Functional Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-40447-4_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,7,3]],"date-time":"2023-07-03T18:04:35Z","timestamp":1688407475000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-40447-4_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642404467","9783642404474"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-40447-4_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}