{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:20:57Z","timestamp":1725456057709},"publisher-location":"Berlin, Heidelberg","reference-count":7,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540590484"},{"type":"electronic","value":"9783540491781"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/bfb0014045","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T07:50:31Z","timestamp":1132732231000},"page":"63-77","source":"Crossref","is-referenced-by-count":2,"title":["Using subtyping in program optimization"],"prefix":"10.1007","author":[{"given":"S.","family":"Berardi","sequence":"first","affiliation":[]},{"given":"L.","family":"Boerio","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,9]]},"reference":[{"key":"5_CR1","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-68952-9","volume-title":"Foundations of Constructive Mathematics","author":"M. Beeson","year":"1985","unstructured":"M. Beeson, Foundations of Constructive Mathematics, Berlin, Springer-Verlag, 1985"},{"key":"5_CR2","unstructured":"S. Berardi, An Application of PER Models to Program Extraction, Technical Report, Turin University, 1992."},{"key":"5_CR3","unstructured":"S. Berardi, Pruning Simply Typed \u03bb-terms, Technical Report, Turin University, 1993."},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"L. Boerio, Extending Pruning Techniques to Polymorphic Second Order \u03bb-Calculus, Proceedings of ESOP '94, Edinburgh, April 1994, LNCS 788, D. Sannella (ed.), Springer-Verlag, pp. 120\u2013134.","DOI":"10.1007\/3-540-57880-3_8"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"C. Paulin-Mohring, Extracting F \u03c9 's Programs from Proofs in the Calculus of Constructions, In: Association for Computing Machinery, editor, Sixteenth Annual ACM Symposium on Priciples of Programming Languages, 1989.","DOI":"10.1145\/75277.75285"},{"key":"5_CR6","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1016\/S0747-7171(08)80139-3","volume":"12","author":"Y. Takayama","year":"1991","unstructured":"Y. Takayama, Extraction of Redundancy-free Programs from Constructive Natural Deduction Proofs, Journal of Symbolic Computation, 1991, 12, 29\u201369","journal-title":"Journal of Symbolic Computation"},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"A. S. Troelstra, Mathematical Investigation of Intuitionistic Arithmetic and Analysis, Lecture Notes in Mathematics, 344, Springer-Verlag, 1973","DOI":"10.1007\/BFb0066739"}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0014045","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T04:37:49Z","timestamp":1586579869000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0014045"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540590484","9783540491781"],"references-count":7,"URL":"https:\/\/doi.org\/10.1007\/bfb0014045","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}