This award is for research on the design and semantics of statically-typed object-oriented programming languages. The project has several goals. (1) It builds on and extends the design of the polymorphic, statically-typed object-oriented programming language, PolyTOIL, to provide more power and expressibility while retaining type-safety. (2) It investigates the design of an object-oriented language whose primary relation between types is matching rather than subtyping. This will likely req uire the development of a partial type-inference system to allow the programmer to avoid the proliferation of bounded type parameters. (3) It seeks to create better mathematical (denotational) models for foundational calculi for object-oriented languages. (4) It investigates the development of verification techniques for object-oriented programming languages. (5) It applies current knowledge of the semantics of object-oriented languages to the understanding of concurrent object-oriented languages. These problems are being attacked using formal specifications of type-checking rules and operational semantics. Subject-reduction-style theorems are being used to prove the safety of type systems. Interpreters are being written in order to provide a better understanding of the strengths and weaknesses of the systems and in order to invetigate scaling up of theoretical designs to full-strength programming languages. The project seeks to validate verification techniques by proving the consistency of an operational and axiomatic semantics.
