1 July - 31 December 1995
Organisers: S Abramsky (Imperial College, London), G Kahn (INRIA, Sophia-Antipolis), J C Mitchell (Stanford), A M Pitts (Cambridge)
Wednesday September 13, 11:00 am
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.