Abstract Dependent Classes
Offered in co-supervision with Nada Amin (University of Cambridge, UK).
Dependent classes  combine the flexibility of dynamic dispatching à la Smalltalk with safety à la Scala. However, a beautiful core that can support abstract methods has still not been devised. A good starting point is the DC calculus of Vaidas Gasiunas' thesis . The exciting insight from the thesis is that subtyping can be described as constraint entailment -- not a new idea in itself, see Frank Pfenning's subtyping lecture notes  but something that hasn't been explored much in an object-oriented setting. The time is ripe due to very efficient constraint solvers (SMT — Satisfiability Modulo Theory).
There are two potential projects.
1. One is a working on an implementation, as a prototype for experimenting with case studies.
2. The other is a formalization in Coq, Agda or Isabelle to assure the proof sketch already outlined in the thesis. There are some old attempts in Isabelle that could serve as a starting point.
If you are interested in any of the above topics or have any further questions, please contact: bracevac -at- st.informatik.tu-darmstadt.de (Oliver Bracevac)