Foundations of Information Technologies

- FIT 2009 -

June 14-27, 2009, Novi Sad

General Information
Courses and Lecture Notes
Local Information




                   Decision problems in polymorphic type assignment

                                                    Pawel Urzyczyn



This talk will survey known results (some old ones and some new ones) and open questions concerning decision problems related to various type-assignment systems. These decision problems fall into essentially two categories:
• Typability and type-checking: Given a term M, determine if M can be assigned a given type (or any type at all) in a given (or arbitrary) type environment.
• Type inhabitation (provability): Given a type t, determine if thereis a term M such that M has type t (or equivalently, if t has a proof) in a given type environment.

For the simply typed lambda-calculus, these problems are decidable in polynomial time (type inference) or space (inhabitation). In polymorphic calculi each of them can be undecidable; in particular the famous theorem of Wells states that typability in system F is undecidable. Little is known about decidable subsystems (or variants) of F, for example it is an open problem if typability is decidable in the parametric fragment.

In addition to the universal polymorphism of system F and its relatives, this survey will cover the decision problems originating from Curry-style, Church-style and domain-free calculi involving other forms of polymorphism: existential, ad hoc (intersection types) and first-order (dependent types).