Isaac Newton Institute for Mathematical Sciences

Semantics of Computation

1 July - 31 December 1995

Organisers: S Abramsky (Imperial College, London), G Kahn (INRIA, Sophia-Antipolis), J C Mitchell (Stanford), A M Pitts (Cambridge)

Semantics of Computation Seminar

Wednesday September 13, 11:00 am

The search for a "good" static-type discipline for object-oriented languages

Kim Bruce
Newton Institute and Williams College

While simple static-typing disciplines exist for some current object-oriented languages, they are often so restrictive for programmers that they are forced to by-pass the type system with type casts. Other languages allow more freedom, but require run-time checking to pick up the type errors that their more permissive systems missed.

In this talk we present a series of sample programs illustrating the limitations of existing type systems, and suggest ways of improving the expressibility of these systems while retaining static type safety. In particular we will discuss the motivations behind introducing "MyType", "matching", and "bounded matching" into these type systems.

The intent is to avoid presenting screenfuls of type-checking rules, but instead explain why the problems are interesting via the series of sample programs. The technical details (including proofs of subject reduction and type safety) are available in papers left on line.

Copyright © Isaac Newton Institute