A type system equivalent to flow analysis

ABSTRACT

Flow-based safety analysis of higher-order languages has been studied by Shivers, and Palsberg and Schwartzbach. Open until now is the problem of finding a type system that accepts exactly the same programs as safety analysis.In this paper we prove that Amadio and Cardelli's type system with subtyping and recursive types accepts the same programs as a certain safety analysis. The proof involves mappings from types to flow information and back. As a result, we obtain an inference algorithm for the type system, thereby solving an open problem.

REFERENCES

• 1: Roberto M. Amadio , Luca Cardelli, Subtyping recursive types, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.4, p.575-631, Sept. 1993 [doi>10.1145/155183.155231]
• 2: Torben Amtoft, Minimal Thunkification, Proceedings of the Third International Workshop on Static Analysis, p.218-229, September 22-24, 1993
• 3: Andrew W. Appel, Compiling with continuations, Cambridge University Press, New York, NY, 1992
• 4: Anders Bondorf, Automatic autoprojection of higher order recursive equations, Science of Computer Programming, v.17 n.1-3, p.3-34, Dec. 1991
• 5: Anders Bondorf and Jesper Jorgensen. Efficient analyses for realistic off-line partial evaluation. Journal of Functional Programming, 3(3):315-346, 1993.
• 6: Charles Consel, A tour of Schism: a partial evaluation system for higher-order applicative languages, Proceedings of the 1993 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.145-154, June 14-16, 1993, Copenhagen, Denmark [doi>10.1145/154630.154645]
• 7: Nevin Heintze. Personal communication. 1994.
• 8: Dexter Kozen , Jens Palsberg , Michael I. Schwartzbach, Efficient recursive subtyping, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.419-428, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158700]
• 9: Dexter Kozen , Jens Palsberg , Michael I. Schwartzbach, Efficient inference of partial types, Journal of Computer and System Sciences, v.49 n.2, p.306-324, Oct. 1994 [doi>10.1016/S0022-0000(05)80051-0]
• 10: Tsung-Min Kuo , Prateek Mishra, Strictness analysis: a new perspective based on type inference, Proceedings of the fourth international conference on Functional programming languages and computer architecture, p.260-272, September 11-13, 1989, Imperial College, London, United Kingdom [doi>10.1145/99370.99390]
• 11: Jens Palsberg, Flobal Program Analysis in Constraint Form, Proceedings of the 19th International Colloquium on Trees in Algebra and Programming, p.276-290, April 11-13, 1994
• 12: Jens Palsberg , Michael I. Schwartzbach, Safety analysis versus type inference, Information and Computation, v.118 n.1, p.128-141, April 1995 [doi>10.1006/inco.1995.1058]
• 13: Jens Palsberg , Michael I. Schwartzbach, Safety analysis versus type inference for partial types, Information Processing Letters, v.43 n.4, p.175-180, Sept. 28, 1992 [doi>10.1016/0020-0190(92)90196-3]
• 14: Jens Palsberg and Michael I. Schwartzbach. Binding-time analysis: Abstract interpretation versus type inference. In Proc. ICCL'9#, Fifth IEEE International Conference on Computer Languages, pages 289-298, Toulouse, France, May 1994.
• 15: Jens Palsberg , Michael I. Schwartzbach, Object-oriented type systems, John Wiley and Sons Ltd., Chichester, UK, 1994
• 16: Olin Shivers. Data-flow analysis and type recovery in Scheme. in Peter Lee, editor, Topics in Advanced Language Implementation, pages 47-87. MIT Press, 1991.
• 17: Yan Mei Tang , Pierre Jouvelot, Separate Abstract Interpretation for Control-Flow Analysis, Proceedings of the International Conference on Theoretical Aspects of Computer Software, p.224-243, April 19-22, 1994
• 18: Mitchell Wand, Finding the source of type errors, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.38-43, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512648]
• 19: Mitchell Wand, Type inference for record concatenation and multiple inheritance, Information and Computation, v.93 n.1, p.1-15, July 1991 [doi>10.1016/0890-5401(91)90050-C]
• 20: Mitchell Wand , Paul Steckler, Selective and lightweight closure conversion, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.435-445, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.178044]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES

  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

General Terms:
Algorithms, Languages, Theory, Verification