Type-checking algorithms

Question

I am starting a personal bibliographic research on type-checking algorithms and want some tips. What are the most commonly used type-checking algorithms, strategies and general techniques?

I am particularly interested in complex type-checking algorithms that were implemented in widely known strongly static typed languages such as, for example, C++, Java 5+, Scala or others. I.E, type-checking algorithms that are not very simple due to the very simple typing of the underlying language (like Java 1.4 and below).

I am not per se interested in a specific language X, Y or Z. I am interested in type-checking algorithms regardless of the language that they target. If you provide a answer like "language L that you never heard about which is strongly typed and the typing is complex has a type-checking algorithm that does A, B and C by checking X and Y using the algorithm Z", or "the strategy X and Y used for Scala and a variant Z of A used for C# are cool because of the R, S and T features that works in that way", then the answers are nice.

Answer 1

Most research does not actually publish the type checking algorithms for full blown programming languages. You will find some formalisations of a large part of the type systems for full programming languages, such as the work done by Drossopoulou and Eisenbach for Java or Nipkov et al's work on C++. More often, though, you will only find the type systems for some core part of the language (Featherweight Java is one example) or for the core concepts of a language such as the local type inference approach of scala.

In conferences such as POPL and ICFP you will find many type checking algorithms for specific kinds of type systems, and novel approaches such as bidirectional and tridirectional type checking.

More generally, you probably need to know about the Damas-Milner algorithm, local type inference, bidirectional and tridirectional type checking, and expand from there, by following references in the papers and by using google scholar to find which papers cite these and build on the approaches described. Also, as suggested above, conferences such as POPL, ICPF, ESOP and even ECOOP and OOPSLA will have papers relevant to your quest.

Answer 2

A basic tool are Attribute Grammars. You will maybe not be able to do every wicked thing you can imagine with them, but they are a good starting point.

Essentially, you can walk over a program's abstract syntax tree top-down and/or bottom-up and pass information around. So, for instance, you could pass global scope type information (e.g. classes and their members) downwards and determine the type of expressions recursively, i.e. bottom-up, passing the resulting types upwards.

Find some explanation and examples in the slides here (Chapter 5).