{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:00:11Z","timestamp":1725483611132},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540657637"},{"type":"electronic","value":"9783540489597"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48959-2_8","type":"book-chapter","created":{"date-parts":[[2007,5,3]],"date-time":"2007-05-03T12:52:16Z","timestamp":1178196736000},"page":"83-97","source":"Crossref","is-referenced-by-count":3,"title":["Useless-Code Detection and Elimination for PCF with Algebraic Data Types"],"prefix":"10.1007","author":[{"given":"Ferruccio","family":"Damiani","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,5,27]]},"reference":[{"issue":"5","key":"8_CR1","doi-asserted-by":"publisher","first-page":"663","DOI":"10.1093\/logcom\/6.5.663","volume":"6","author":"S. Berardi","year":"1996","unstructured":"S. Berardi. Pruning Simply Typed Lambda Terms. Journal of Logic and Computation, 6(5):663\u2013681, 1996.","journal-title":"Journal of Logic and Computation"},{"key":"8_CR2","series-title":"Lect Notes Comput Sci","volume-title":"TLCA\u201995","author":"S. Berardi","year":"1995","unstructured":"S. Berardi and L. Boerio. Using Subtyping in Program Optimization. In TLCA\u201995, LNCS 902. Springer9Verlag, 1995."},{"key":"8_CR3","series-title":"Lect Notes Comput Sci","volume-title":"TLCA\u201997","author":"S. Berardi","year":"1997","unstructured":"S. Berardi and L. Boerio. Minimum Information Code in a Pure Functional Language with Data Types. In TLCA\u201997, LNCS 1210. Springer-Verlag, 1997. 83, 83, 84, 96, 96, 96, 96, 96, 97"},{"doi-asserted-by":"crossref","unstructured":"S. K. Biswas. A Demand-Driven Set-Based Analysis. In POPL\u201997, pages 372\u2013385. ACM, 1997.","key":"8_CR4","DOI":"10.1145\/263699.263753"},{"unstructured":"L. Boerio. Optimizing Programs Extracted from Proofs. PhD thesis, Universit\u00e0 di Torino, 1995.","key":"8_CR5"},{"key":"8_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1007\/3-540-61739-6_39","volume-title":"SAS\u201996","author":"M. Coppo","year":"1996","unstructured":"M. Coppo, F. Damiani, and P. Giannini. Refinement Types for Program Analysis. In SAS\u201996, LNCS 1145, pages 143\u2013158. Springer-Verlag, 1996."},{"unstructured":"F. Damiani. Non-standard type inference for functional programs. PhD thesis, Universit\u00e0 di Torino, February 1998.","key":"8_CR7"},{"key":"8_CR8","series-title":"Lect Notes Comput Sci","volume-title":"TYPES\u201996","author":"F. Damiani","year":"1998","unstructured":"F. Damiani and F. Prost. Detecting and Removing Dead Code using Rank 2 Intersection. In TYPES\u201996, LNCS 1512. Springer-Verlag, 1998."},{"key":"8_CR9","volume-title":"The Coq Proof Assistant Reference Manual Version 6.2","author":"B. Barras","year":"1998","unstructured":"B. Barras et al. The Coq Proof Assistant Reference Manual Version 6.2. INRIA-Rocquencourt-CNRS-ENS Lyon, may 1998."},{"unstructured":"A. D. Gordon. Bisimilarity as a Theory of Functional Programs. Mini-Course. Technical Report NS-95-3 BRICS Notes Series, Computer Science Department of Aarhus University, 1995.","key":"8_CR10"},{"unstructured":"G. Kahn. Natural semantics. In K. Fuchi and M. Nivat, editors, Programming Of Future Generation Computer. Elsevier Sciences B.V. (North-Holland), 1988.","key":"8_CR11"},{"doi-asserted-by":"crossref","unstructured":"C. Paulin-Mohring. Extracting F\u03c9\u2019s Programs from Proofs in the Calculus of Constructions. In POPL\u201989. ACM, 1989.","key":"8_CR12","DOI":"10.1145\/75277.75285"},{"doi-asserted-by":"crossref","unstructured":"A. M. Pitts. Operationally-based theories of program equivalence. In A. M. Pitts and P. Dybjer, editors, Semantics and Logics of Computation, pages 241\u2013298. Cambridge University Press, 1997.","key":"8_CR13","DOI":"10.1017\/CBO9780511526619.007"},{"issue":"3","key":"8_CR14","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1016\/0304-3975(77)90044-5","volume":"5","author":"G. D. Plotkin","year":"1977","unstructured":"G. D. Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5(3):223\u2013255, 1977.","journal-title":"Theoretical Computer Science"},{"unstructured":"G. D. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, Aarhus University, 1981.","key":"8_CR15"},{"key":"8_CR16","doi-asserted-by":"publisher","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, 12:29\u201369, 1991.","journal-title":"Journal of Symbolic Computation"}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48959-2_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,16]],"date-time":"2019-02-16T07:07:31Z","timestamp":1550300851000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48959-2_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540657637","9783540489597"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-48959-2_8","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}