Typing for the programmer's convenience

[Shriram Krishnamurthi <address@hidden>]

Reginald Braithwaite-Lee wrote:

> Is anyone working on typing systems from the perspective of program
> correctness? Can anyone provide some reference materials for study?

How about the last thirty years of so of type theory?

A good starting point would be Benjamin Pierce's recent book, which
provides a nice compendium of the basic material you would need to
understand contemporary research.

Interestingly, type systems have come a full circle -- from being a
way to help compiler writers allocate space to focusing on program
((very) partial) correctness, they are returning to the problems of
compiler direction, synthesizing the two viewpoints.  See, for
instance, the work on typed assembly languages (don't snigger).

Nice quote, btw.

Shriram