PolyTOIL
- 1 March 2003
- journal article
- Published by Association for Computing Machinery (ACM) in ACM Transactions on Programming Languages and Systems
- Vol. 25 (2), 225-290
- https://doi.org/10.1145/641888.641891
Abstract
PolyTOIL is a new statically typed polymorphic object-oriented programming language that is provably typesafe. By separating the definitions of subtyping and inheritance, providing a name for the type of self, and carefully defining the type-checking rules, we have obtained a language that is very expressive while supporting modular type-checking of classes. The matching relation on types, which is related to F-bounded quantification, is used both in stating type-checking rules and expressing the bounds on type parameters for polymorphism. The design of PolyTOIL is based on a careful formal definition of type-checking rules and semantics. A proof of type safety is obtained with the aid of a subject reduction theorem.Keywords
This publication has 21 references indexed in Scilit:
- Foundations of Object-Oriented LanguagesInformation and Computation, 2002
- Integrating subtyping, matching and type quantification: A practical perspectivePublished by Springer Science and Business Media LLC ,1996
- Bounded Quantification Is UndecidableInformation and Computation, 1994
- A paradigmatic object-oriented programming language: Design, static typing and semanticsJournal of Functional Programming, 1994
- Safe and decidable type checking in an object-oriented languageACM SIGPLAN Notices, 1993
- Subtyping recursive typesACM Transactions on Programming Languages and Systems, 1993
- Recursion over realizability structuresInformation and Computation, 1991
- A modest model of records, inheritance, and bounded quantificationInformation and Computation, 1990
- A semantics of multiple inheritanceInformation and Computation, 1988
- On understanding types, data abstraction, and polymorphismACM Computing Surveys, 1985