Abstract Dependent Classes

Abstract Dependent Classes

Master Thesis

Offered in co-supervision with Nada Amin (University of Cambridge, UK).

Dependent classes [1] 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 [2]. 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 [3] 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.


[1] http://www.informatik.uni-marburg.de/~kos/papers/depcls-oopsla07.pdf

[2] https://tubiblio.ulb.tu-darmstadt.de/48187/

[3] https://www.cs.cmu.edu/~fp/courses/15312-f04/handouts/14-subtyping.pdf

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)