Bounded quantifiers have interval models

ABSTRACT

We propose a sound model for an extension of the language Fun, proposed by L. Cardelli and P. Wegner as a formalization of the notion of inheritance in the context of higher order polymorphic functional 1anguages. The model is obtained by modifying the Interval Model proposed by R. Cartwright, in order to accommodate bounded quantifiers and to obtain a sound structure. Our extension of the language supports also a general recursion operator for functions (but not for types).

REFERENCES

• 1: Amadio R. {1988} 'A fixed point extension to the polymorphic lambda calculus", IEEE Conference on Log/c 01 Computer Science 88, Edinburgh, July.
• 2: Bruce K,, Longo G, {1988} "A modest model of records, inheritance and bounded quantification", IEEE Conference on Logic in Computer Science 88, Edinburgh, July.
• 3: Kim B. Bruce , Albert R. Meyer, The semantics of second order polymorphic lambda calculus., Proc. of the international symposium on Semantics of data types, p.131-156, July 1984, Sophia-Antipolis, France
• 4: Kim B. Bruce , Albert R. Meyer , John C. Mitchell, The semantics of second-order lambda calculus, Information and Computation, v.85 n.1, p.76-134, March 1990 [doi>10.1016/0890-5401(90)90044-I]
• 5: CardeUi L. {1984} 'A semantics of rnultiple inheritance~, Intl. and Computation, to appear.
• 6: 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]
• 7: L. Cardelli, Structural subtyping and the notion of power type, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.70-79, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73566]
• 8: Robert Cartwright, Types as intervals, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.22-36, January 14-16, 1985, New Orleans, Louisiana, United States [doi>10.1145/318593.318604]
• 9: Dezanl M., Vennerl B. {1987} 'Partial types and intervals', preprtnt, Dip. di Informatica, Universit~ di Torino, October.
• 10: Girard, J. {1972} Interpretation fonclionelle et elimination des coupures darts l'arithmetique d'ordre superieur, Th~se de Doctorat d'Etat, Paris.
• 11: G Longo , S Martini, Computability in higher types, P&ohgr; and the completeness of type assignment, Theoretical Computer Science, v.46 n.2-3, p.197-217, Oct. 1986
• 12: David MacQueen , Gordon Plotkin , Ravi Sethi, An ideal model for recursive polymorphic types, Information and Control, v.71 n.1-2, p.95-130, Oct/Nov. 1986 [doi>10.1016/S0019-9958(86)80019-5]
• 13: Simone Martini, An Interval Model for Second-Order Lambda Calculus, Category Theory and Computer Science, p.219-237, September 07-09, 1987
• 14: Martini S. {1988} ModeUl non estensionali del polimorfismo in programmazione funzionale, tesl di Dottorato dt Ricerca, Unlversita di Pisa, January.
• 15: Milner R. {1978} ',% theory of type polymorphism in progrmnming', Journal of Computer and Systems Sc~, 3 (348-375).
• 16: John Mitchell, Type inference and type containment., Proc. of the international symposium on Semantics of data types, p.257-277, July 1984, Sophia-Antipolis, France
• 17: Andrew M. Pitts, Polymorphism is Set Theoretic, Constructively, Category Theory and Computer Science, p.12-39, September 07-09, 1987
• 18: John C. Reynolds, Towards a theory of type structure, Programming Symposium, Proceedings Colloque sur la Programmation, p.408-423, April 09-11, 1974
• 19: Seely R.A.G. {1986} 'Categorical semantics for higher order polymorphic lambda calculus", J. of Symbolic Logic, vol 52, n. 4 (Dec 87), 969-989.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Applicative (functional) languages

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Procedures, functions, and subroutines

General Terms:
Algorithms, Design, Languages