That was a longer hiatus than I had intended. Partly because not everything went according to plan.
My original plan was that, upon returning from my vacation, I would spend my remaining time at EPFL writing a technical report explaining everything I knew about the problems with Scala Classic. Instead, on my first day back in the office, Martin came by with a draft of a new formal system, DOT (for Dependent Object Types), that he came up with while he was on vacation. After about four weeks I managed to root out pretty much all of the obvious problems with DOT, but another four weeks was not enough to get the proofs and the metatheory into a state that we were happy with. I am not really sure what will happen with DOT in the long term.
There are a few clever things about DOT that avoid some of the problems I encountered with Scala Classic. For example, Scala Classic only had intersection types while DOT has both intersection and union types, which solves some problems with computing the members of types. However, with Scala Classic I was trying to model a minimal subset Scala language as it exists, without adding any new features that many never be supported by the full language. I have no idea if we will see union types in the actual Scala implementation anytime soon.
The other thing DOT does is give up the goal of trying to be a minimal subset of Scala and throws out quite a few important things from a user perspective. For example, there are no methods (only λ-abstractions), no existentials, no built-in inheritance or mix-in composition (though you can encode it by hand), and object fields must be syntactically values.
This last restriction is particularly important because it solves by fiat the problems that arose in Scala Classic from using paths that have an empty type in dependent type projections. However, it also means that you may not be able to directly encode some Scala programs into DOT without an effect or termination analysis. Therefore, while DOT has the potential to be a useful intermediary step, there will still be more work to be done to provide a semantics for a more realistic subset of the Scala language.
I have been in Copenhagen for a little over a month now, but I am not really ready to comment on the research I have been doing here yet. So in the meantime I'll probably focus more on fonts and typography.
I have unfortunately been quite busy the past several months, and have not had as much time to write about what I have been doing as I would have liked. For the most part, I have been splitting my time between teaching and research. I will hopefully go into more detail about the latter in the near future.
However, I figured I should take some time now, before I leave for my first proper vacation in a year, to announce that I have accepted a postdoc position at ITU in Copenhagen with Carsten Schürmann. This has been in the works for a while now, but this week I finally was able to make it official. My plan is to start at ITU at the beginning of March, where I will be working on things relating to the LF family of logical frameworks, Twelf, and Delphin.
There are probably a vanishingly small number of you that care about what this means for Scala Classic, but I hope to write something much more detailed about it when I get back from my vacation. I'll leave you in suspense with the short answer: despite all my efforts, it simply is not possible to prove it sound without making it a very different language. Which is rather unfortunate.
Several weeks ago I decided that instead of calling the core calculus that I have been working on Featherweight Scala, which could be confusing given that there is already a different calculus with that name, that I would call it Scala Classic.
I had hoped to submit a paper on Scala Classic to POPL 2009, but it has been taking too long to work out the metatheory. Partly because I am developing a mechanized proof of type soundness in Twelf, and on my first attempt at representing heaps I think tried to be too clever. However, a more traditional treatment of heaps leads to the need to explicitly represent typing contexts, rather than the implicit treatment of contexts more commonly used in Twelf.
This afternoon I finally finished the proof of the theorem that is traditionally called "substitution". However, the proof of type preservation will also require another theorem formalizing a substitution-like property for singleton types. I am hoping that I can prove that theorem more quickly now that I've built up all the explicit context theory. I have not thought much about whether there are any unusual theorems needed to prove progress.
In any event, I would ideally have the proofs finished by the beginning of August. My current plan is to try submitting the paper to PLDI (which is even in Europe this year), unless some obviously better venue comes to my attention.
One of the reasons I would really like to have the proofs done by August is that I will be teaching a PhD level course here at EPFL this fall on mechanized sepcifications and proofs, with a strong emphasis on deductive systems. It also looks like I may fill in some for a masters level course based on TAPL. So between those two things, I am not going to have nearly as much time for research as would be ideal.