Abstract
In this paper we extend, by allowing the use of rank 2 intersection, the non-standard type assignment system for the detection and elimination of dead-code in typed functional programs presented by Coppo et al in the Static Analysis Symposium '96. The main application of this method is the optimization of programs extracted from proofs in logical frameworks, but it could be used as well in the elimination of dead-code determined by program specialization. The use of nonstandard types (also called annotated types) allows to exploit the type structure of the language for investigating program properties. Dead-code is detected via annotated type inference, which can be performed in a complete way, by reducing it to the solution of a system of inequalities between annotation variables. Even though the language considered in the paper is the simply typed λ-calculus with cartesian product, if-then-else, fixpoint, and arithmetic constants we can generalize our approach to polymorphic languages like Miranda, Haskell, and CAML.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
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–940, 1983.
B. Barras, S. Boutin, C. Cornes, J. Courant, J.-C. Filliâtre, H. Herbelin, G. Huet, P. Manoury, C. Muñoz, 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.
P. N. Benton. Strictness Analysis of Lazy Functional Programs. PhD thesis, University of Cambridge, Pembroke College, 1992.
S. Berardi. Pruning Simply Typed Lambda Terms, 1993. Internal report. Dipartimento di Informatica, Universitá di Torino.
S. Berardi. Pruning Simply Typed Lambda Terms. Journal of Logic and Computation, 6(5):663–681, 1996.
S. Berardi and L. Boerio. Using Subtyping in Program Optimization. In Typed Lambda Calculus and Applications, 1995.
L. Boerio. Optimizing Programs Extracted from Proofs. PhD thesis, Universitá di Torino, 1995.
G. Castagna. Covariance and contravariance: conflict without a cause. ACM Transactions on Programming Languages and Systems, 17(3):431–447, 1995.
G. Castagna. Object-Oriented Programming: A Unified Foudation. Progress in Theoretical Computer Science Series. Birkhauser, Boston, December 1996.
M. Coppo, F. Damiani, and P. Giannini. Refinment Types for Program Analysis. In SAS'96, LNCS 1145, pages 143–158. Springer, 1996.
M. Coppo, F. Damiani, and P. Giannini. On Strictness and Totality. In TACS'97, LNCS 1281, pages 138–164. Springer, 1997.
M. Coppo and M. Dezani-Ciancaglini. An extension of basic functional theory for lambda-calculus. Notre Dame Journal of Formal Logic, 21(4):685–693, 1980.
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–135. Springer, 1995.
F. Damiani. Non-standard type inference for the static analysis of lazy functional programs. PhD thesis, Universitá di Torino. In preparation.
F. Damiani and P. Giannini. An Inference Algorithm for Strictness. In TLCA'97, LNCS 1210, pages 129–146. Springer, 1997.
C. Hankin and D. Le Métayer. Deriving algorithms for type inference systems: Applications to strictness analysis. In POPL'94, pages 202–212. ACM, 1994.
C. Hankin and D. Le Métayer. Lazy type inference and program analysis. Science of Computer Programming, 25:219–249, 1995.
T. P. Jensen. Abstract Interpretation in Logical Form. PhD thesis, University of London, Imperial College, 1992.
G. Kahn. Natural semantics. In K. Fuchi and M. Nivat, editors, Programming Of Future Generation Computer. Elsevier Sciences B. V. (North-Holland), 1988.
T. M. Kuo and P. Mishra. Strictness analysis: a new perspective based on type inference. In Functional Programming Languages and Computer Architecture, pages 260–272. ACM, 1989.
Z. Luo and R. Pollack. Lego proof development system: User's manual. Technical Report ECS-LFCS-92-211, University of Edinburgh., 1992.
J. Palsberg and P. O'Keefe. A Type System Equivalent to Flow Analysis. In POPL'95, pages 367–378. ACM, 1995.
C. Paulin-Mohring. Extracting F ω's Programs from Proofs in the Calculus of Constructions. In POPL'89. ACM, 1989.
C. Paulin-Mohring. Extraction des Programmes dans le Calcul des Constructions. PhD thesis, Université Paris VII, 1989.
A. M. Pitts. Operationally-based theories of program equivalence. In A. M. Pitts and P. Dybjer, editors, Semantics and Logics of Computation, pages 241–298. Cambridge University Press, 1997.
F. Prost. Marking techniques for extraction. Technical Report RR95-47, Ecole Normale Supérieure de Lyon, Lyon, December 1995.
K. L. Solberg. Annotated Type Systems for Program Analysis. PhD thesis, Aarhus University, Denmark, 1995. Revised version.
Y. Takayama. Extraction of Redundancy-free Programs from Constructive Natural Deduction Proofs. Journal of Symbolic Computation, 12:29–69, 1991.
S. van Bakel. Intersection Type Disciplines in Lambda Calculus and Applicative Term Rewriting Systems. PhD thesis, Katholieke Universiteit Nijmegen, 1993.
D. A. Wright. Reduction Types and Intensionality in the Lambda-Calculus. PhD thesis, University of Tasmania, 1992.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Damiani, F., Prost, F. (1998). Detecting and removing dead-code using rank 2 intersection. In: Giménez, E., Paulin-Mohring, C. (eds) Types for Proofs and Programs. TYPES 1996. Lecture Notes in Computer Science, vol 1512. Springer, Berlin, Heidelberg . https://doi.org/10.1007/BFb0097787
Download citation
DOI: https://doi.org/10.1007/BFb0097787
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65137-6
Online ISBN: 978-3-540-49562-8
eBook Packages: Springer Book Archive