{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:11:55Z","timestamp":1725664315641},"publisher-location":"Berlin, Heidelberg","reference-count":9,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540617808"},{"type":"electronic","value":"9783540707226"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61780-9_65","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T22:25:35Z","timestamp":1330295135000},"page":"105-119","source":"Crossref","is-referenced-by-count":0,"title":["First order marked types"],"prefix":"10.1007","author":[{"given":"Philippe","family":"Curmin","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"8_CR1","unstructured":"S. Berardi, Pruning Simply Typed \u03bb-terms, Technical Report, Turin University, 1993."},{"key":"8_CR2","series-title":"LNCS","volume-title":"Proceedings of TLCA '95","author":"S. Berardi","year":"1995","unstructured":"S. Berardi and L. Boerio, Using Subtyping in Program Optimization, Proceedings of TLCA '95, Edinburgh, April 1995, LNCS, Springer-Verlag."},{"key":"8_CR3","series-title":"LNCS 788","first-page":"120","volume-title":"Proceedings of ESOP '94","author":"L. Boerio","year":"1994","unstructured":"L. Boerio, Extending Pruning Techniques to Polymorphic Second Order \u03bb-Calculus, Proceedings of ESOP '94, Edinburgh, Avril 1994, LNCS 788, D. Sannella (ed.), Springer-Verlag, pp. 120\u2013134."},{"key":"8_CR4","unstructured":"C. Goad, Computational Uses of the Manipulation of Formal Proofs, Stanford Technical Report CS-80-819, 1980."},{"key":"8_CR5","unstructured":"S. Hayashi and H. Nakano, PX: A Computational Logic, The MIT Press, 1988."},{"key":"8_CR6","unstructured":"S. Hayashi and Y. Takayama \u201dLifschitz's Logic of Calculable Numbers and Optimizations in Program Extraction\u201d, 1994, LNCS 792, Springer Verlag."},{"key":"8_CR7","first-page":"146","volume":"26","author":"J.L. Krivine","year":"1990","unstructured":"J.L. Krivine and M. Parigot, Programming with proofs, J. Inform. Process. Cybern. EIK 26 (1990) 146\u2013167.","journal-title":"J. Inform. Process. Cybern. EIK"},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"Ch. 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 Principles of Programming Languages, 1989.","DOI":"10.1145\/75277.75285"},{"key":"8_CR9","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"}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61780-9_65.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:10:54Z","timestamp":1605647454000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61780-9_65"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540617808","9783540707226"],"references-count":9,"URL":"https:\/\/doi.org\/10.1007\/3-540-61780-9_65","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}