Hi everybody =) First time I write to the list. My name is Glauber and I'm doing my master course at UNICAMP, Brazil, under supervisor of Prof. Dr. Arnaldo Vieira Moura. I'm interested in Haskell, type theory and algebraic specification (formal methods). I've been studying these subjects to my Computer-Science-Bachelor-degree-final work. It was an implementation of an homomorphism between a little constructive algebraic specification code (based mainly in Loeckx's Specification of Abstract Data Types) and a Haskell code. SableCC was used as tool to implement the interpreter because I've already used it before. One theme to work one should be implementing this in Haskell itself, but there is already HasCASL. I've already contacted the HasCASL professors and I'm reading more about the project. At the same time, I want to look for some theme under type theory, too. The main concern about HasCASL is that I want to get in deep touch with functional programming during my master thesis and I'm not sure (yet) if studying HasCASL would get me there. I've reading some papers about type theory and Haskell (mainly the ones suggested in the haskell.org site) and as I could see the topics are very interesting. I'm not sure, however, if there is something that can be done in a 2-year-master course. Mainly, they propose new extensions that have became new languages (Cayenne, Omega and Epigram). Other topic I'd like to get in touch is theorem proving. As I could see, Coq and Isabelle are the most used with Haskell. Indeed, HasCASL use Isabelle and this could be a nice thing to work on, as was suggested by HasCASL professors. As I know that lots of you here are researchers, I'd like to ask some opinions about what can be done as a master thesis having in mind that I want to continue in a PhD course after the master one. Sorry if the email is too large. And thank for the patience and for any opinion you can give me. Yours, Glauber.