Decidable bounded quantification

ABSTRACT

The standard formulation of bounded quantification, system F≤, is difficult to work with and lacks important syntactic properties, such as decidability. More tractable variants have been studied, but those studied so far either exclude significant classes of useful programs or lack a compelling semantics. We propose here a simple variant of F≤ that ameliorates these difficulties. It has a natural semantic interpretation, enjoys a number of important properties that fail in F≤, and includes all of the programming examples for which F≤ has been used in practice.

REFERENCES

• Ama91: R. Amadio. Recursion and Subtyping in Lambda Calcuh. PhD thesis, Universit~ degli Studi di Pisa, 1991.
• BM92: Kim Bruce , John C. Mitchell, PER models of subtyping, recursive types and higher-order polymorphism, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.316-327, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143230]
• Bru93: Kim B. Bruce, Safe type checking in a statically-typed object-oriented programming language, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.285-298, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158650]
• BTCGS91: Val Breazu-Tannen , Thierry Coquand , Carl A. Gunter , Andre Scedrov, Inheritance as implicit coercion, Information and Computation, v.93 n.1, p.172-221, July 1991 [doi>10.1016/0890-5401(91)90055-7]
• Car92: Luca Cardelli. Extensible records in a pure calculus of subtyping. Research report 81, DEC Systems Research Center, January 1992. To appear in {GM93}.
• Car93: L. Cardelli. An implementation of F<. Technical Report 97, Digital Equipment Corporation, February 1993.
• CD80: M. Coppo and M. Dezani-Ciancaglini. An extension of the basic functionality theory for the A-calculus. Notre-Dame Journal of Formal Logic, 21(4):685-693, October 1980.
• CG92: P.L. Curien and G. Ghelli. Coherence of subsumption, minimum typing and the type checking in F<. Mathematical Structures in Computer Science, 2(1), 1992.
• CW85: Luca Cardelli , Peter Wegner, On understanding types, data abstraction, and polymorphism, ACM Computing Surveys (CSUR), v.17 n.4, p.471-523, Dec. 1985 [doi>10.1145/6041.6042]
• dB72: Nicolas G. de Bruijn. Lambda-calculus notation with nameless dummies: a tool for automatic formula manipulation with application to the Church-Rosser theorem. Indag. Math., 34(5):381-392, 1972.
• Ghe90: G. Ghelli. Proof Theoretic Studies about a Minimal Type System Integrating Inclusion and Parametrzc Polymorphism. PhD thesis, Dipartimento di Informatica, Universit~ di Pisa, March 1990. Tech. Rep. TD-6/90.
• Ghe93a: G. Ghelli. Divergence of F < type-checking. Technical Report 5/93, Dipartimento d'Informatica, Universit~ degli Studi di Pisa, 1993.
• Ghe93b: Giorgio Ghelli, Recursive Types Are not Conservative over F, Proceedings of the International Conference on Typed Lambda Calculi and Applications, p.146-162, March 16-18, 1993
• Ghe93c: G. Ghelli. S-All-Loc is not transitive. Mail to the TYPES mailing fist, February 1993.
• Gir72: J-Y. Girard. Interpretation fonctionelle et ~limination des coupures dans l'arithm~tique d'ordre sup~rieur. Th~se de doctorat d'~tat, 1972. Universit~ Paris VII.
• GM93: Carl A. Gunter , John C. Mitchell, Theoretical aspects of object-oriented programming: types, semantics, and language design, MIT Press, Cambridge, MA, 1994
• GP93: G. Ghelli and B. Pierce. Bounded existentials and minimal typing. Draft report, Dipartimento d'Informatica Universith di Pisa, 1993. Unpublished.
• KS92: D. Katiyar and S. Sankar. Completely bounded quantification is decidable. In Proceedings of the A CM SIGPLAN Workshop on ML and its Apphcations, pages 68-77, San Francisco, June 1992.
• Mit90: John C. Mitchell, Toward a typed foundation for method specialization and inheritance, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.109-124, December 1989, San Francisco, California, United States [doi>10.1145/96709.96719]
• Pie91: Benjamin Crawford Pierce, Programming with intersection types and bounded polymorphism, Carnegie Mellon University, Pittsburgh, PA, 1992
• Pie93: B.C. Pierce. Bounded quantification is undecidable. In 20th Ann. A CM Syrup. on Principles of Programming Languages. ACM-Press, 1993.
• PT93: Benjamin C. Pierce , David N. Turner, Object-oriented programming without recursive types, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.299-312, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158653]
• Rey74: John C. Reynolds, Towards a theory of type structure, Programming Symposium, Proceedings Colloque sur la Programmation, p.408-423, April 09-11, 1974
• Rey88: J.C. Reynolds. Preliminary design of the programming language Forsythe. Technical Report CMU-CS-88-159, Carnegie Mellon University, June 1988.
• Rey91: John C. Reynolds, The Coherence of Languages with Intersection Types, Proceedings of the International Conference on Theoretical Aspects of Computer Software, p.675-700, September 24-27, 1991

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

General Terms:
Theory, Verification