{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T14:01:41Z","timestamp":1725804101465},"publisher-location":"Cham","reference-count":5,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319118628"},{"type":"electronic","value":"9783319118635"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-11863-5_5","type":"book-chapter","created":{"date-parts":[[2014,8,28]],"date-time":"2014-08-28T04:43:41Z","timestamp":1409201021000},"page":"62-76","source":"Crossref","is-referenced-by-count":1,"title":["Case of (Quite) Painless Dependently Typed Programming: Fully Certified Merge Sort in Agda"],"prefix":"10.1007","author":[{"given":"Ernesto","family":"Copello","sequence":"first","affiliation":[]},{"given":"\u00c1lvaro","family":"Tasistro","sequence":"additional","affiliation":[]},{"given":"Bruno","family":"Bianchi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"5_CR1","unstructured":"Altenkirch, T., McBride, C., McKinna, J.: Why dependent types matter (2005), http:\/\/www.e-pig.org\/downloads\/ydtm.pdf"},{"key":"5_CR2","doi-asserted-by":"publisher","first-page":"552","DOI":"10.1017\/S095679681300018X","volume":"23","author":"E. Brady","year":"2013","unstructured":"Brady, E.: Idris, a general-purpose dependently typed programming language: Design and implementation. Journal of Functional Programming\u00a023, 552\u2013593 (2013)","journal-title":"Journal of Functional Programming"},{"key":"5_CR3","unstructured":"The coq proof assistant reference manual (2009)"},{"issue":"12","key":"5_CR4","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1145\/2578854.2503786","volume":"48","author":"S. Lindley","year":"2013","unstructured":"Lindley, S., McBride, C.: Hasochism: The pleasure and pain of dependently typed haskell programming. SIGPLAN Not.\u00a048(12), 81\u201392 (2013)","journal-title":"SIGPLAN Not."},{"key":"5_CR5","unstructured":"Norell, U.: Towards a practical programming language based on dependent type theory, Ph.D. thesis (2007)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-11863-5_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,23]],"date-time":"2020-08-23T20:15:23Z","timestamp":1598213723000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-11863-5_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319118628","9783319118635"],"references-count":5,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-11863-5_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}