[Haskell-cafe] About functional programing, type theory and a master thesis topic

[Glauber Cabral]

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.