Thomas Jensen
Abstract
We describe how binding-time, data-flow, and strictness analyses for languages with higher-order functions and algebraic data types can be obtained by instantiating a generic program logic and axiomatization of the properties analyzed for. A distinctive feature of the analyses is that disjunctions of program properties are represented exactly. This yields analyses of high precision and provides a logical characterization of abstract interpretations involving tensor products and uniform properties of recursive data structures. An effective method for proving properties of a program based on fixed-point iteration is obtained by grouping logically equivalent formulae of the same type into equivalence classes, obtaining a lattice of properties of that type, and then defining an abstract interpretation over these lattices. We demonstrate this in the case of strictness analysis by proving that the strictness abstract interpretation of a program is the equivalence class containing the strongest property provable of the program in the strictness logic.
- ABRAMSKY, S. 1991a. A domain equation for bisimulation. Inf. Comput. 92, 2, 161-218. Google Scholar
- ABRAMSKY, S. 1991b. Domain theory in logical form. Ann. Pure Appl. Logic 51, 1-77.Google Scholar
- AIKEN, t., WIMMERS, E. L., AND LAKSHMAN, T. I~. 1994. Soft typing with conditional types. In Proceedings of the 21st Annual A CM Symposium on Principles of Programming Languages. ACM Press, New York, 163-173. Google Scholar
- BANDELT, H.-J. 1980. The tensor product of continuous lattices. Mathematische Zeitschrift 172, 89-96.Google Scholar
- BARBANERA, F., DEZANI-CIANCAGLINI, M., AND DE'LIGUORO, W. 1995. Intersection and union types: Syntax and semantics. Inf. Comput. 119, 202-230. Google Scholar
- BENTON, P. N. 1992a. Strictness analysis and optimising transformations for lazy functional programs. Ph.D. thesis, Univ. of Cambridge, Cambridge, U.K.Google Scholar
- BENTON, P. N. 1992b. Strictness logic and polymorphic invariance. In Proceedings of the 2nd International Symposium on Logical Foundations of Computer Science, A. Nerode and M. Taitslin, Eds. Lecture Notes in Computer Science, vol. 620. Springer Verlag, Berlin. Google Scholar
- BENTON, P. N. 1993. Strictness properties of lazy algebraic datatypes. In Static Analysis, P. C. et. al., Ed. Lecture Notes in Computer Science, vol. 724. Springer Verlag, Berlin. Google Scholar
- BURN, G. L. 1991. Lazy Functional Languages: Abstract Interpretation and Compilation. Research Monographs in Parallel and Distributed Computing. Pitman, London, U.K. Google Scholar
- BURN, G. L. 1992. Properties of abstract interpretation techniques. Tech. Rep. Doc 92/19, Imperial College, Univ. of London, London, U.K.Google Scholar
- BURN, G. L., HANKIN, C., AND ABRAMSKY, S. 1986. The theory and practice of strictness analysis for higher order functions. Sci. Comput. Program. 7, 249-278.Google Scholar
- COUSOT, P. AND COUSOT, R. 1976. Static determination of dynamic properties of programs. In Proceedings of the 2nd International Symposium on Programming. Dunod, Paris, France, 106-130.Google Scholar
- COUSOT, P. AND COUSOT, R. 1979. Systematic design of program analysis frameworks. In Proceedings of the 6th A CM Symposium on Principles of Programming Languages. ACM Press, New York, 269-282. Google Scholar
- COUSOT, P. AND COUSOT, R. 1992. Comparing the Galois connection and widening/narrowing approach to abstract interpretation. Tech. Rep. LIX/RR/92/09, Ecole Polytechnique, Palaiseau, France.Google Scholar
- COUSOT, P. AND COUSOT, R. 1994. Higher-order abstract interpretation (and application to comportment analysis generalising strictness, termination, projection and PER analysis of functional languages). In Proceedings of the 5th IEEE International Conference on Computer Languages, H. Bal, Ed. IEEE Press, New York, 95-112.Google Scholar
- DAVEY, B. AND PRIESTLEY, H. 1990. Introduction to Lattices and Order. Cambridge University Press, Cambridge, U.K.Google Scholar
- DE LAVALETTE, G. R. R. 1992. Strictness analysis via abstract interpretation for recursively defined types. Inf. Comput. 99, 154-177. Google Scholar
- DEUTSCH, t. 1992. Operational models of programming languages and representations of relations on regular languages with application to the static determination of dynamic aliasing properties of data. Ph.D. thesis, Univ. Paris VI, Paris, France.Google Scholar
- ERNOULT, C. AND MYCROFT, A. 1991. Uniform ideals and strictness analysis. In Proceedings of the 18th International Colloqium on Automata, Languages and Programming. Lecture Notes in Computer Science, vol. 510. Springer Verlag, Berlin, 47-59. Google Scholar
- FERGUSON, t. AND HUGHES, J. 1989. An iterative powerdomain construction. In Functional Programming. Proceedings of the 1989 Glasgow workshop, K. Davis and J. Hughes, Eds. Springer Verlag, Berlin. Google Scholar
- FILI~, G. AND RANZATO, F. 1994. Improving abstract interpretations by systematic lifting to the powerset. In Logic Programming--Proceedings of the 1994 International Symposium, M. Bruynooghe, Ed. The MIT Press, Cambridge, Mass., 655-669. Google Scholar
- GUNTER, C. AND SCOTT, D. 1990. Semantic domains. In Handbook of Theoretical Computer Science, J. van Leeuwen, Ed. Vol. B, Formal Models and Semantics. North-Holland, Amsterdam. Google Scholar
- HANKIN, C. AND LE MI~TAYER, D. 1994. Deriving algorithms from type inference systems: Applications to strictness analysis. In Proceedings of the 21st Symposium on Principles of Programming Languages. ACM Press, New York, 202-212. Google Scholar
- HANKIN, C. AND LE MI~TAYER, D. 1995. Lazy type inference and program analysis. Sci. Comput. Program. 25, 219-249. Google Scholar
- HECHT, M. S. 1977. Flow Analysis of Computer Programs. Programming Languages Series. North-Holland, New York. Google Scholar
- HUNT, S. 1991. Abstract interpretation of functional languages: From theory to practice. Ph.D. thesis, Imperial College, Univ. of London, London, U.K.Google Scholar
- HUNT, S. AND SANDS, D. 1991. Binding time analysis: A new PERspective. In Proceedings of the A CM Symposium on Partial Evaluation and Semantics-Based Program Manipulation. ACM Press, New York. Google Scholar
- JENSEN, K. D., HJ_/ERESEN, P., AND ROSENDAHL, M. 1994. Efficient strictness analysis of Haskell. In Proceedings of the 1st International Static Analysis Symposium (SAS'9g), B. Le Charlier, Ed. Lecture Notes in Computer Science, vol. 864. Springer-Verlag, Berlin, 346-362.Google Scholar
- JENSEN, T. 1991. Strictness analysis in logical form. In Proceedings of the 5th ACM Conference on Functional Programming Languages and Computer Architecture, J. Hughes, Ed. Lecture Notes in Computer Science, vol. 523. Springer-Verlag, Berlin, 352-366. Google Scholar
- JENSEN, T. 1992a. Abstract interpretation in logical form. Ph.D. thesis, Imperial College, Univ. of London, London, U.K.Google Scholar
- JENSEN, T. 1992b. Axiomatising uniform properties of recursive data structures. In Proceedings of the 2nd Bordeaux Workshop on Static Analysis, M. Billaud, P. Cast6ran, M. Corsini, K. Musumbu, and A. Rauzy, Eds. Bigre no. 81-82. IRISA, Rennes, France.Google Scholar
- JENSEN, T. 1992c. Disjunctive strictness analysis. In Proceedings of the 7th IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, Calif.Google Scholar
- JENSEN, T. 1994. Abstract interpretation over algebraic data types. In Proceedings of the 5th IEEE International Conference on Computer Languages, H. Bal, Ed. IEEE Press, New York.Google Scholar
- JENSEN, T. 1995. Conjunctive type systems and abstract interpretation of higher-order functional programs. J. Logic Comput. 5, 4, 397-421.Google Scholar
- JONES, N., GOMARD, C., AND SESTOFT, P. 1993. Partial Evaluation and Automatic Program Generation. Series in Computer Science. Prentice-Hall International, Chichester, U.K. Google Scholar
- JONES, N. AND MUCHNICK, S. 1981. Complexity of flow analysis, inductive assertion synthesis and a language due to Dijkstra. In Program Flow Analysis: Theory and Applications, N. Jones and S. Muchnick, Eds. Prentice-Hall, Englewood Cliffs, N.J.Google Scholar
- JONES, N., SESTOFT, P., AND SONDERGAARD, H. 1985. An experiment in partial evaluation: Th e generation of a compiler generator. In Rewriting Techniques and Applications, J. P. Jouannaud, Ed. Lecture Notes in Computer Science, vol. 202. Springer-Verlag, Berlin, 124- 140. Google Scholar
- JONES, N. D. AND MYCROFT, A. 1986. Data flow analysis of applicative programs using minimal function graphs. In Proceedings of the 13th A CM Symposium on Principles of Programming Languages. ACM Press, New York, 296-306. Google Scholar
- LAUNCHBURY, J. 1989. Projection factorisations in partial evaluation. Ph.D. thesis, Dept. of Computing, Univ. of Glasgow, Glasgow, Scotland.Google Scholar
- LE ~/{}~TAYER, D. 1995. Proving properties of programs defined over recursive data structures. In Proceedings of the A CM Symposium on Partial Evaluation and Semantics-Based Program Manipulation, W. Scherlis, Ed. ACM Press, New York, 88-99. Google Scholar
- LEUNG, A. AND ~/{ISHRA, P. 1991. Reasoning about simple and exhaustive demand in higherorder lazy languages. In Proceedings of the 5th A CM Conference on Functional Programming Languages and Computer Architecture, J. Hughes, Ed. Lecture Notes in Computer Science, vol. 523. Springer-Verlag, Berlin. Google Scholar
- OGENSEN, T. 1988. Partially static structures in a self-applicable partial evMuator. In Partial Eva luation and Mixed Computation, D. Bj~rner, A. P. Ershov, and N. D. Jones, Eds. North- Holland, Amsterdam, 325-347.Google Scholar
- iVONSUEZ, B. 1995. Using abstract interpretation to define a strictness type inference system. In Proceedings of the A CM Symposium on Partial Evaluation and Semantics-Based Program Manipulation, W. Scherlis, Ed. ACM Press, New York, 122-133. Google Scholar
- UYLAERT-FILHO, J. 1994. Abstract interpretation in continuation passing style. Ph.D. thesis, Imperial College, Univ. of London, London, U.K.Google Scholar
- NIELSON, F. 1982. A denotationM framework for data flow analysis. Acta Informatica 18, 265-287.Google Scholar
- NIELSON, F. 1984. Abstract interpretation using domain theory. Ph.D. thesis, Univ. of Edinburgh, Edinburgh, Scotland.Google Scholar
- NIELSON, F. 1985. Tensor products generalize the relational data flow analysis method. In Proceedings of the ~th Hungarian Computer Science Conference. 211-225.Google Scholar
- NIELSON, F. AND NIELSON, H. R. 1994. The tensor product in Wadler's analysis of lists. Sci. Comput. Program. 22, 327-354. Google Scholar
- NIELSON, H. R. AND NIELSON, F. 1992. The tensor product in Wadler's analysis of lists. In Proceedings of the ~th European Symposium on Programming, B. Krieg-Briickner, Ed. Lecture Notes in Computer Science, vol. 582. Springer-Verlag, Berlin. Google Scholar
- PLOTKIN, G. D. 1976. A powerdomain construction. SIAM J. Comput. 5, 3, 452-487.Google Scholar
- REYNOLDS, J. C. 1974. On the relation between direct and continuation semantics. In Proceedings of the 2nd International Conference on Algorithms, Languages and Programming. Lecture Notes in Computer Science, vol. 14. Springer-Verlag, Berlin, 141-156. Google Scholar
- ROSENDAHL, ~/{. 1993. Higher-order chaotic iteration sequences. In Proceedings of Programming Language Implementation and Logic Programming (PLILP'93), M. Bruynooghe and J. Penjam, Eds. Lecture Notes in Computer Science, vol. 714. Springer-Verlag, Berlin, 332-345. Google Scholar
- SINTZOFF, ~/{. 1972. Calculating properties of programs by valuations on specific models. Proceedings of the A CM Conference on Proving Assertions about Programs. SIGPLAN Notices 7, 1, 203-207. Google Scholar
- WADLER, P. 1987. Strictness analysis in non-flat domains (by abstract interpretation over finite domains). In Abstract Interpretation of Declarative Languages, S. Abramsky and C. Hankin, Eds. Ellis Horwood, Chichester, U.K.Google Scholar
- WADLER, P. AND HUGHES, R. J. ~/{. 1987. Projections for strictness analysis. In Proceedings of the Conference on Functional Programming and Computer Architecture. Lecture Notes in Computer Science, vol. 274. Springer-Verlag, Berlin. Google Scholar
- WINSKEL, G. 1983. Powerdomains and modMity. In Foundations of Computation Theory, M. Karpinski, Ed. Lecture Notes in Computer Science, vol. 158. Springer-Verlag, Berlin. Google Scholar
Index Terms
- Disjunctive program analysis for algebraic data types
Recommendations
Derivation and inference of higher-order strictness types
We extend an existing first-order typing system for strictness analysis to the fully higher-order case, covering both the derivation system and the inference algorithm. The resulting strictness typing system has expressive capabilities far beyond that ...
Completeness and Cut-elimination in the Intuitionistic Theory of Types
In this paper we define a model theory and give a semantic proof of cut-elimination for ICTT, an intuitionistic formulation of Church's theory of types defined by Miller et al. and the basis for the λProlog programming language. Our approach, extending ...
A typed lambda calculus with intersection types
Intersection types are well known to type theorists mainly for two reasons. Firstly, they type all and only the strongly normalizable lambda terms. Secondly, the intersection type operator is a meta-level operator, that is, there is no direct logical ...
Reviews
D. John Cooke
Jensen presents a framework for analyzing uniform program properties (relating to the content of data structures rather than to the structures themselves) in a high-order functional language with recursive data structures. The development starts from a set of general (logic and type-specific) rules and from rules that pertain to the particular analysis being undertaken. Strictness is the central property under consideration throughout, but other properties considered include binding time and dataflow analyses. Notation is a potential problem in any work that bridges so many topics. The “box” and “diamond” symbols have nonstandard interpretations as do t (here indicating that we know everything—no specific information) and f (here indicating “undefined”). These are reasonable, but initially confusing, particularly because t and f are distinct from the Boolean constants. The author does point this out. For each expression in the language, we can derive a normal form consisting of a disjunction of irreducible formulas. Entailment gives rise to provable equality, which is then used to quotient out equivalent expressions, giving a partial-order semantics. Hence, we can calculate an abstract interpretation for each expression in terms of lower sets. Although there are issues that make direct application of the theory impractical, the results are interesting and can be used in conjunction with the work of others. The paper is well motivated and includes adequate explanations. The relationship between this research and the work of others is discussed at length. I ts association with tensor products is particularly relevant.
Access critical reviews of Computing literature here
Become a reviewer for Computing Reviews.
Comments