{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:35Z","timestamp":1761611195048},"publisher-location":"Berlin, Heidelberg","reference-count":30,"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\/bfb0097787","type":"book-chapter","created":{"date-parts":[[2006,11,24]],"date-time":"2006-11-24T09:27:48Z","timestamp":1164360468000},"page":"66-87","source":"Crossref","is-referenced-by-count":4,"title":["Detecting and removing dead-code using rank 2 intersection"],"prefix":"10.1007","author":[{"given":"Ferruccio","family":"Damiani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fr\u00e9d\u00e9ric","family":"Prost","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,10,26]]},"reference":[{"key":"5_CR1","doi-asserted-by":"publisher","first-page":"931","DOI":"10.2307\/2273659","volume":"48","author":"H. P. Barendregt","year":"1983","unstructured":"H. P. Barendregt, M. Coppo, and M. Dezani-Ciancaglini. A filter lambda model and the completeness of type assignment. Journal of Symbolic Logic, 48:931\u2013940, 1983.","journal-title":"Journal of Symbolic Logic"},{"key":"5_CR2","volume-title":"The Coq Proof Assistant Reference Manual Version 6.1.","author":"B. Barras","year":"1996","unstructured":"B. Barras, S. Boutin, C. Cornes, J. Courant, J.-C. Filli\u00e2tre, H. Herbelin, G. Huet, P. Manoury, C. Mu\u00f1oz, C. Murthy, C. Parent, C. Paulin-Mohring, A. Saibi, and B. Werner. The Coq Proof Assistant Reference Manual Version 6.1. INRIA-Rocquencourt-CNRS-ENS, Lyon, December 1996."},{"key":"5_CR3","unstructured":"P. N. Benton. Strictness Analysis of Lazy Functional Programs. PhD thesis, University of Cambridge, Pembroke College, 1992."},{"key":"5_CR4","unstructured":"S. Berardi. Pruning Simply Typed Lambda Terms, 1993. Internal report. Dipartimento di Informatica, Universit\u00e1 di Torino."},{"issue":"5","key":"5_CR5","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":"5_CR6","doi-asserted-by":"crossref","unstructured":"S. Berardi and L. Boerio. Using Subtyping in Program Optimization. In Typed Lambda Calculus and Applications, 1995.","DOI":"10.1007\/BFb0014045"},{"key":"5_CR7","unstructured":"L. Boerio. Optimizing Programs Extracted from Proofs. PhD thesis, Universit\u00e1 di Torino, 1995."},{"issue":"3","key":"5_CR8","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1145\/203095.203096","volume":"17","author":"G. Castagna","year":"1995","unstructured":"G. Castagna. Covariance and contravariance: conflict without a cause. ACM Transactions on Programming Languages and Systems, 17(3):431\u2013447, 1995.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"5_CR9","volume-title":"Progress in Theoretical Computer Science Series","author":"G. Castagna","year":"1996","unstructured":"G. Castagna. Object-Oriented Programming: A Unified Foudation. Progress in Theoretical Computer Science Series. Birkhauser, Boston, December 1996."},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"M. Coppo, F. Damiani, and P. Giannini. Refinment Types for Program Analysis. In SAS'96, LNCS 1145, pages 143\u2013158. Springer, 1996.","DOI":"10.1007\/3-540-61739-6_39"},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"M. Coppo, F. Damiani, and P. Giannini. On Strictness and Totality. In TACS'97, LNCS 1281, pages 138\u2013164. Springer, 1997.","DOI":"10.1007\/BFb0014550"},{"issue":"4","key":"5_CR12","doi-asserted-by":"publisher","first-page":"685","DOI":"10.1305\/ndjfl\/1093883253","volume":"21","author":"M. Coppo","year":"1980","unstructured":"M. Coppo and M. Dezani-Ciancaglini. An extension of basic functional theory for lambda-calculus. Notre Dame Journal of Formal Logic, 21(4):685\u2013693, 1980.","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"D. Dussart and F. Henglein and C. Mossin. Polymorphic Recursion and Sub-type Qualifications: Polymorphic Binding-Time Analysis in Polynomial Time. In SAS'95, LNCS 983, pages 118\u2013135. Springer, 1995.","DOI":"10.1007\/3-540-60360-3_36"},{"key":"5_CR14","unstructured":"F. Damiani. Non-standard type inference for the static analysis of lazy functional programs. PhD thesis, Universit\u00e1 di Torino. In preparation."},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"F. Damiani and P. Giannini. An Inference Algorithm for Strictness. In TLCA'97, LNCS 1210, pages 129\u2013146. Springer, 1997.","DOI":"10.1007\/3-540-62688-3_33"},{"key":"5_CR16","doi-asserted-by":"crossref","unstructured":"C. Hankin and D. Le M\u00e9tayer. Deriving algorithms for type inference systems: Applications to strictness analysis. In POPL'94, pages 202\u2013212. ACM, 1994.","DOI":"10.1145\/174675.177858"},{"key":"5_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":"5_CR18","unstructured":"T. P. Jensen. Abstract Interpretation in Logical Form. PhD thesis, University of London, Imperial College, 1992."},{"key":"5_CR19","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":"5_CR20","doi-asserted-by":"crossref","unstructured":"T. M. Kuo and P. Mishra. Strictness analysis: a new perspective based on type inference. In Functional Programming Languages and Computer Architecture, pages 260\u2013272. ACM, 1989.","DOI":"10.1145\/99370.99390"},{"key":"5_CR21","unstructured":"Z. Luo and R. Pollack. Lego proof development system: User's manual. Technical Report ECS-LFCS-92-211, University of Edinburgh., 1992."},{"key":"5_CR22","doi-asserted-by":"crossref","unstructured":"J. Palsberg and P. O'Keefe. A Type System Equivalent to Flow Analysis. In POPL'95, pages 367\u2013378. ACM, 1995.","DOI":"10.1145\/199448.199533"},{"key":"5_CR23","doi-asserted-by":"crossref","unstructured":"C. Paulin-Mohring. Extracting F \u03c9's Programs from Proofs in the Calculus of Constructions. In POPL'89. ACM, 1989.","DOI":"10.1145\/75277.75285"},{"key":"5_CR24","unstructured":"C. Paulin-Mohring. Extraction des Programmes dans le Calcul des Constructions. PhD thesis, Universit\u00e9 Paris VII, 1989."},{"key":"5_CR25","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.","DOI":"10.1017\/CBO9780511526619.007"},{"key":"5_CR26","series-title":"Technical Report RR95-47","volume-title":"Marking techniques for extraction","author":"F. Prost","year":"1995","unstructured":"F. Prost. Marking techniques for extraction. Technical Report RR95-47, Ecole Normale Sup\u00e9rieure de Lyon, Lyon, December 1995."},{"key":"5_CR27","volume-title":"Annotated Type Systems for Program Analysis","author":"K. L. Solberg","year":"1995","unstructured":"K. L. Solberg. Annotated Type Systems for Program Analysis. PhD thesis, Aarhus University, Denmark, 1995. Revised version."},{"key":"5_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":"5_CR29","volume-title":"Intersection Type Disciplines in Lambda Calculus and Applicative Term Rewriting Systems","author":"S. Bakel van","year":"1993","unstructured":"S. van Bakel. Intersection Type Disciplines in Lambda Calculus and Applicative Term Rewriting Systems. PhD thesis, Katholieke Universiteit Nijmegen, 1993."},{"key":"5_CR30","unstructured":"D. A. Wright. Reduction Types and Intensionality in the Lambda-Calculus. PhD thesis, University of Tasmania, 1992."}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0097787","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,22]],"date-time":"2019-04-22T10:53:54Z","timestamp":1555930434000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0097787"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540651376","9783540495628"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/bfb0097787","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}