{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T18:28:05Z","timestamp":1725474485158},"publisher-location":"Berlin, Heidelberg","reference-count":5,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540651376"},{"type":"electronic","value":"9783540495628"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0097801","type":"book-chapter","created":{"date-parts":[[2006,11,24]],"date-time":"2006-11-24T14:27:48Z","timestamp":1164378468000},"page":"354-372","source":"Crossref","is-referenced-by-count":5,"title":["Abstract insertion sort in an extension of type theory with record types and subtyping"],"prefix":"10.1007","author":[{"given":"Alvaro","family":"Tasistro","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,10,26]]},"reference":[{"key":"19_CR1","doi-asserted-by":"crossref","unstructured":"Betarte G., Tasistro A. Extension of Martin-L\u00f6f's type theory with record types and subtyping. In Proceedings of the Conference \u201c25 Years of Constructive Type Theory\u201d, Oxford University Press, 1997.","DOI":"10.1007\/BFb0097801"},{"key":"19_CR2","unstructured":"Coquand, Th., Nordstr\u00f6m B., Smith J. M., von Sydow B. Type theory and programming. EATCS 52, 1994."},{"key":"19_CR3","unstructured":"Knuth D. The art of computer programming. Vol. 3: Sorting and searching. Addison Wesley, 1973."},{"key":"19_CR4","unstructured":"Martin-L\u00f6f P. Philosophical implications of type theory. Lectures given at the Facolt\u00e1 de Lettere e Filosofia, Universit\u00e1 degli Studi di Firenze, Florence, March 15th.\u2013May 15th., 1987. Privately circulated notes."},{"key":"19_CR5","unstructured":"Nordstr\u00f6m B., Petersson K., Smith J. M. Programming in Martin-L\u00f6f's type theory. An introduction. Oxford Science Publications, 1990."}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0097801","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,22]],"date-time":"2019-04-22T14:53:40Z","timestamp":1555944820000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0097801"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540651376","9783540495628"],"references-count":5,"URL":"https:\/\/doi.org\/10.1007\/bfb0097801","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}