A General Framework for Hindley/Milner Systems with Constraints

Type systems are important tools in the design, analysis, and verification of programming languages. A particular interesting type system is the Hindley/Milnersystem for which numerous, ad-hoc extensions exist.

I co-developed a general Hindley/Milner framework, baptized HM(X) [49,47], parameterized in terms of the constraint domain X. Specific instances can be obtained by appropriately defining X. I applied this framework to study the design of record systems [48] and to solve the open problem of type inference for dimension types [41]. I also gave a reformulation of HM(X) where the concept of substitutions is replaced by constraints [46]. My PhD thesis [45] contains a comprehensive summary.



Martin Sulzmann 2006-07-19