So, after a long pause, I’ll start to blog again. And, since my last post was about the so called Maniac Spring, where I’ve set some ambitious objectives, let’s see what I’ve finished:

• Work on some unpublished results of my thesis. I’ve spent little time with this topic, since after almost 5 years working in type inference for Haskell, I’m tired of such stuff. Because of that, I’ve put this aside. But this was good, since now I have some ideas on how to improve type inference in the presence of Generalised Algebraic Data Types. I probably start some implementation of these ideas really soon.
• Supervise two students to produce publishable results. This was a bit problematic due to some problems, but, I believe that still time to get something to SBLP 2015 — Brazilian Symposium on Programming Languages.
• Continue to write a discrete mathematics book, for the classes that I teach on UFOP. At least, one objective was achieved. I’ve finished a first book draft which is available here.
• Prepare my classes of Discrete Mathematics and Formal Language Theory. These are also done.
• Continue to study dependently typed languages, specially Agda. I’ve spent a lot of time programming in Agda lately. Soon I’ll continue to write more about my Agda related adventures.
• Study the Holy Trinity of computer science. Since, during my PhD, I’ve studied a lot of type systems, I focused on learning Proof Theory and Category Theory. I’ve spent a lot of time trying to formalize proof theory results in Agda. I’m having difficulties on how to represent contexts in order to get a appropriate representation of sequent calculus. But this I’ll be a subject of a future post.

I did not get all tasks finished, but I believe that setting those objectives helped me to get focused on them or on a subset of them.