{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:18:33Z","timestamp":1725549513024},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540253044"},{"type":"electronic","value":"9783540318620"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-31862-0_25","type":"book-chapter","created":{"date-parts":[[2010,3,12]],"date-time":"2010-03-12T08:28:55Z","timestamp":1268382535000},"page":"341-355","source":"Crossref","is-referenced-by-count":6,"title":["Random Generators for Dependent Types"],"prefix":"10.1007","author":[{"given":"Peter","family":"Dybjer","sequence":"first","affiliation":[]},{"given":"Qiao","family":"Haiyan","sequence":"additional","affiliation":[]},{"given":"Makoto","family":"Takeyama","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"25_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","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 \u2014 an introduction. In: Swierstra, S.D., Oliveira, J.N. (eds.) AFP 1998. LNCS, vol.\u00a01608, pp. 28\u2013115. Springer, Heidelberg (1999), Revised version of lecture notes for AFP 1998"},{"key":"25_CR2","unstructured":"Benke, M.: Towards generic programming in type theory. Presentation at Annual ESPRIT BRA TYPES Meeting, Berg en Dal. Submitted for publication (April 2002), available from \n                    \n                      http:\/\/www.cs.chalmers.se\/~marcin\/Papers\/Notes\/nijmegen.ps.gz"},{"key":"25_CR3","first-page":"265","volume":"10","author":"M. Benke","year":"2003","unstructured":"Benke, M., Dybjer, P., Jansson, P.: Universes for generic programs and proofs in dependent type theory. Nordic Journal of Computing\u00a010, 265\u2013289 (2003)","journal-title":"Nordic Journal of Computing"},{"key":"25_CR4","series-title":"ACM Sigplan Notices","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1145\/351240.351266","volume-title":"Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP-00)","author":"K. Claessen","year":"2000","unstructured":"Claessen, K., Hughes, J.: QuickCheck: a lightweight tool for random testing of Haskell programs. In: Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP-2000). ACM Sigplan Notices, vol.\u00a035.9, pp. 268\u2013279. ACM Press, New York (2000)"},{"key":"25_CR5","unstructured":"Coquand, C.: The Agda homepage, \n                    \n                      http:\/\/www.cs.chalmers.se\/~catarina\/agda"},{"key":"25_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/3-540-44904-3_8","volume-title":"Typed Lambda Calculi and Applications","author":"T. Coquand","year":"2003","unstructured":"Coquand, T., Pollack, R., Takeyama, M.: A logical framework with dependently typed records. In: Hofmann, M.O. (ed.) TLCA 2003. LNCS, vol.\u00a02701, pp. 105\u2013119. Springer, Heidelberg (2003)"},{"issue":"4","key":"25_CR7","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1007\/BF01211308","volume":"6","author":"P. Dybjer","year":"1994","unstructured":"Dybjer, P.: Inductive families. Formal Aspects of Computing\u00a06(4), 440\u2013465 (1994)","journal-title":"Formal Aspects of Computing"},{"key":"25_CR8","doi-asserted-by":"crossref","unstructured":"Dybjer, P.: A general formulation of simultaneous inductive-recursive definitions in type theory. Journal of Symbolic Logic\u00a065 (June 2000)","DOI":"10.2307\/2586554"},{"key":"25_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/10930755_12","volume-title":"Theorem Proving in Higher Order Logics","author":"P. Dybjer","year":"2003","unstructured":"Dybjer, P., Haiyan, Q., Takeyama, M.: Combining testing and proving in dependent type theory. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol.\u00a02758, pp. 188\u2013203. Springer, Heidelberg (2003)"},{"key":"25_CR10","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1109\/QSIC.2003.1319111","volume-title":"Proceedings of Third International Conference on Quality Software","author":"P. Dybjer","year":"2003","unstructured":"Dybjer, P., Haiyan, Q., Takeyama, M.: Verifying Haskell programs by combining testing and proving. In: Proceedings of Third International Conference on Quality Software, pp. 272\u2013279. IEEE Press, Los Alamitos (2003)"},{"issue":"1","key":"25_CR11","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/BF03037052","volume":"2","author":"M. Hagiya","year":"1984","unstructured":"Hagiya, M., Sakurai, T.: Foundation of logic programming based on inductive definition. New Generation Comput (JAPAN) ISSN: 0288-3635\u00a02(1), 59\u201377 (1984) ISSN: 0288-3635 QA 76 N 48","journal-title":"New Generation Comput. (JAPAN) ISSN: 0288-3635"},{"key":"25_CR12","unstructured":"Hallgren, T.: The Alfa homepage, \n                    \n                      http:\/\/www.cs.chalmers.se\/~hallgren\/Alfa"},{"key":"25_CR13","volume-title":"Programming in Martin-L\u00f6f type theory: an introduction","author":"B. Nordstr\u00f6m","year":"1990","unstructured":"Nordstr\u00f6m, B., Petersson, K., Smith, J.M.: Programming in Martin-L\u00f6f type theory: an introduction. Oxford University Press, Oxford (1990)"},{"key":"25_CR14","unstructured":"Pfenning, F., Sch\u00fcrmann, C.: The Twelf homepage, \n                    \n                      http:\/\/www-2.cs.cmu.edu\/~twelf\/"},{"key":"25_CR15","unstructured":"Haiyan, Q.: Testing and Proving in Dependent Type Theory. PhD thesis, Chalmers University of Technology (2003)"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing - ICTAC 2004"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-31862-0_25.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,18]],"date-time":"2020-11-18T23:30:01Z","timestamp":1605742201000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-31862-0_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540253044","9783540318620"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-31862-0_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}