{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,9]],"date-time":"2026-03-09T22:59:09Z","timestamp":1773097149996,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540410546","type":"print"},{"value":"9783540453505","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-45350-4_13","type":"book-chapter","created":{"date-parts":[[2007,8,11]],"date-time":"2007-08-11T05:45:53Z","timestamp":1186811153000},"page":"172-189","source":"Crossref","is-referenced-by-count":9,"title":["Type-Based Useless-Code Elimination for Functional Programs Position Paper"],"prefix":"10.1007","author":[{"given":"Stefano","family":"Berardi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mario","family":"Coppo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ferruccio","family":"Damiani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Paola","family":"Giannini","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,6,1]]},"reference":[{"key":"13_CR1","unstructured":"A. V. Aho, R. Sethi, and J. Ullmann. Complilers: Principles, Techniques, and Tools. Addison Wesley, 1986."},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"M. J. Beeson. Foundations of Constructive Mathematics, Metamathematical Studies. Springer, 1985.","DOI":"10.1007\/978-3-642-68952-9"},{"key":"13_CR3","unstructured":"S. Berardi. Pruning Simply Typed Lambda Terms, 1993. Course notes of the\u201cSummer School in Logic and Programming\u201d, University of Chambery."},{"issue":"5","key":"13_CR4","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":"13_CR5","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. Springer, 1995."},{"key":"13_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"30","DOI":"10.1007\/3-540-62688-3_27","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, pages 30\u201345. Springer, 1997."},{"key":"13_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"120","DOI":"10.1007\/3-540-57880-3_8","volume-title":"ESOP\u201994","author":"L. Boerio","year":"1994","unstructured":"L. Boerio. Extending Pruning Techniques to Polymorphic Second Order \u03bb-calculus. In ESOP\u201994, LNCS 788, pages 120\u2013134. Springer, 1994."},{"key":"13_CR8","unstructured":"L. Boerio. Optimizing Programs Extracted from Proofs. PhD thesis, Universit\u00e0 di Torino, 1995."},{"key":"13_CR9","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, 1996."},{"key":"13_CR10","unstructured":"F. Damiani. Non-standard type inference for functional programs. PhD thesis, Dipartimento di Informatica, Universit\u00e0 di Torino, February 1998."},{"key":"13_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1007\/3-540-48959-2_8","volume-title":"TLCA\u201999","author":"F. Damiani","year":"1999","unstructured":"F. Damiani. Useless-code detection and elimination for PCF with algebraic Datatypes. In TLCA\u201999, LNCS 1581, pages 83\u201397. Springer, 1999."},{"key":"13_CR12","first-page":"271","volume":"8","author":"F. Damiani","year":"2000","unstructured":"F. Damiani. Conjunctive types and useless-code elimination (extended abstract). In ICALP Workshops, volume 8 of Proceedings in Informatics, pages 271\u2013285. Carleton-Scientific, 2000.","journal-title":"ICALP Workshops"},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"F. Damiani and P. Giannini. Automatic useless-code elimination for HOT functional programs. Journal of Functional programming. To appear.","DOI":"10.1017\/S0956796800003786"},{"key":"13_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1007\/BFb0097787","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, pages 66\u201387. Springer, 1998."},{"key":"13_CR15","unstructured":"A. Fischbach and J. Hannan. Type Systems and Algoritms for Useless-Variable Elimination, 1999. Submitted."},{"key":"13_CR16","unstructured":"C. A. Goad. Computational uses of the manipulation of proofs. PhD thesis, Stanford University, 1980."},{"key":"13_CR17","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1016\/0167-6423(95)00012-7","volume":"25","author":"C. Hankin","year":"1995","unstructured":"C. Hankin and D. Le M\u00e9tayer. Lazy type inference and program analysis. Science of Computer Programming, 25:219\u2013249, 1995.","journal-title":"Science of Computer Programming"},{"key":"13_CR18","unstructured":"N. Kobayashi. Type-Based Useless Variable Elimination. In PEPM\u201900. ACM, 2000. To appear."},{"key":"13_CR19","doi-asserted-by":"crossref","unstructured":"G. Kreisel and A. Troelstra. Formal systems for some branches of intionistic analysis. Annals of Pure and Applied Logic, 1, 1979.","DOI":"10.1016\/0003-4843(70)90001-X"},{"key":"13_CR20","doi-asserted-by":"crossref","unstructured":"F. Nielson. Annotated type and effect systems. ACM Computing Surveys vol. 28 no. 2, 1996. (Invited position statement for the Symposium on Models of Programming Languages and Computation).","DOI":"10.1145\/234528.234745"},{"key":"13_CR21","doi-asserted-by":"crossref","unstructured":"F. Nielson, H. R. Nielson, and C. Hankin. Principles of Program Analysis. In preparation, http:\/\/www.daimi.au.dk\/~hrn\/PPA\/ppa.html , 1999.","DOI":"10.1007\/978-3-662-03811-6"},{"key":"13_CR22","doi-asserted-by":"crossref","unstructured":"C. Paulin-Mohring. Extracting Fw\u2019s Programs from Proofs in the Calculus of Constructions. In POPL\u201989. ACM, 1989.","DOI":"10.1145\/75277.75285"},{"key":"13_CR23","unstructured":"C. Paulin-Mohring. Extraction de Programme dans le Calcul des Constructions. PhD thesis, Universit\u00e9 Paris VII, 1989."},{"issue":"3","key":"13_CR24","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"},{"key":"13_CR25","doi-asserted-by":"crossref","unstructured":"F. Prost. Aform alization of static analyses in system F. In ed]H. Ganzinger, editor, Automated Deduction \u2013 CADE-16, 16th International Conference on Automated Deduction, LNAI 1632. Springer-Verlag, 1999.","DOI":"10.1007\/3-540-48660-7_22"},{"key":"13_CR26","unstructured":"F. Prost. As tatic calculus of dependencies for the \u03bb-cube. In Proc. of IEEE 15th Ann. Symp. on Logic in Computer Science (LICS\u20192000). IEEE Computer Society Press, 2000. To appear."},{"key":"13_CR27","unstructured":"O. Shivers. Control Flow Analysis of Higher-Order Languages. PhD thesis, Carnegie-Mellon University, 1991."},{"key":"13_CR28","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"},{"key":"13_CR29","doi-asserted-by":"crossref","unstructured":"A. Troelstra, editor. Metamathematical Investigation of Intuitionistic Arithmetic and Analysis. LNM 344. Springer, 1973.","DOI":"10.1007\/BFb0066739"},{"key":"13_CR30","doi-asserted-by":"crossref","unstructured":"M. Wand and I. Siveroni. Constraints Systems for Useless Variable Elimination. In POPL\u201999, pages 291\u2013302. ACM, 1999.","DOI":"10.1145\/292540.292567"},{"key":"13_CR31","unstructured":"R. Wilhelm and D. Maurer. Compliler Design. Addison Wesley, 1995."},{"key":"13_CR32","doi-asserted-by":"crossref","unstructured":"H. Xi. Dead Code Elimination through Dependent Types. In PADL\u201999, pages 228\u2013242, 1999.","DOI":"10.1007\/3-540-49201-1_16"}],"container-title":["Lecture Notes in Computer Science","Semantics, Applications, and Implementation of Program Generation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45350-4_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T19:03:14Z","timestamp":1556737394000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45350-4_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540410546","9783540453505"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/3-540-45350-4_13","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2000]]}}}