There are various interesting open questions in type theory and lambda calculus and their applications. This builds on knowledge you have acquired in the course "Semantics and Rewriting" (IBC025) and the Master course "Type Theory and Coq" (IMC010).
One can evaluate lambda calculus in call-by-name, call-by-value, call-by-need and call-by-push-value style. How to understand and use these and what is the complexity of algorithms using that evaluation model? This is (still) a very active field.
Contact: Herman Geuvers
The Curry-Howard formulas-as-types isomorphism is between proofs in constructive logic and typed lambda terms, which can be viewed as functional programs. Extending this isomorphism to classical logic, we can interpret classical proofs as "functional programs with jumps", which can me modeled as escape or call-cc constructs. There has been done a lot of work on the extension of formulas-as-types to classical logic, giving rise to new presentations of the logical systems, new typed lambda calculi, new reduction rules and new reduction strategies. In all these areas (or in the combination of them) there are still many open questions left.
Contact: Herman Geuvers
The most recent advancement in type theory is HoTT (Homotopy Type Theory), which aims at giving a "Univalent Foundations of Mathematics". It also aims at giving a better treatment of various fundamental concepts from computer science, like "data types with laws" and "equivalence of data". An important concept to work with these are so called "higher inductive types".
Contact: Herman Geuvers
Together with Tonny Hurkens I have been working on finding a general procedure to derive deduction rules from truth tables, both for classical and for constructive logic. These are viewed and studied as typed lambda calculi, following the formulas-as-types interpretation. We have written an introductory paper on this and an extended paper, but lots of questions remain and lots of generalizations are still possible, e.g. how to describe cut-elimination (proof reduction) for classical logic, how to define a general proof term interpretation for classical logic, how to extend this to predicate logic, ... A master thesis (in mathematics) on the topic has been written by Iris van der Giessen.
Contact: Herman Geuvers
De Bruijn, who was a genius, once defined a system called Lambda-Delta (or Delta-Lambda, depending on the paper that you look at). However, this was before type theory got its present form, and therefore these systems do not resemble the current systems at all. Now Philippe de Groote once had a paper in which he gave a "more modern" version of these systems, but that was rather skimpy. A possible project would be to (a) explicitly prove that the system by de Bruijn indeed corresponds to the system by de Groote and (b) to implement this system efficiently. Also, it would be interesting to relate this system to the modern type theories, or to create a variant that is closer to the more modern systems.
Contact: Freek Wiedijk
Herman and Freek had a paper about explicit conversions in which a type theory was defined in which the conversions needed to type check a term were represented in the proof term. More recently Benno van den Berg and Martijn den Besten defined objective type theory, in which the conversions are represented by propositional equalities. A possible project would be to study and compare both systems, to establish whether there is a relation between the two.
Contact: Freek Wiedijk and Herman Geuvers