This project continues a study of type systems for the -calculus and functional programming languages. The emphasis is on type- reconstruction problems. Algebraic characterizations of type- reconstruction problems give rise to new and more general forms of unification, often with applications in other areas of computer science. Together with type-reconstruction problems, the expressive powers of the formalisms considered are to be compared and calibrated. Principal topics include: generalized type structures (especially polymorphism, coercions, existential types), decision procedures for unification problems and their complexity, programming features characterized by complexity classes.
