# Maniac Spring Results

** Published:**

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.