Thesis Idea

The immediate point of my foray into ATP is for my Bachelors Thesis. My current working idea is to employ ACL2 to prove theorems about Haskell programs. Proving theorems about any Haskell program would be far too difficult a project for something to be completed within 2 years (I graduate in Spring '09), so at the moment I am evaluating what subset of Haskell I wish to work on.

I'd like to have a subset that captures at least SOME of the interesting properties of Haskell. Some of the features I'm considering include:

1. Infinite objects
   
2. Lazy evaluation (specifically call-by-need)
3. Static typing
4. Type inference
5. Currying
6. Pattern Matching

Modeling any of these features in ACL2 presents a challenge in and of itself.

#1 is tricky since ACL2 itself only has finite objects, so reasoning about the properties of infinite objects without creating an instance of such a creature won't be simple. Fortunately, Matt Kaufmann did some work in this area back in the 80's for adapting Nqthm (predecessor to ACL2) into a theorem prover about the SASL language. He just put up a soft copy of a tech report he wrote on the subject (exactly 1 year and 1 day before I was born...) here.

#2 Shouldn't be too tricky. Since the subset of Haskell I'll be using will be completely side-effect free, I can model call-by-need with call-by-name and maintain correctness.

#3 The hard part about including this would be handling types in the untyped ACL2. I'm not sure how to go about this, but it seems like someone has probably worked on this before, so I can base my work on previous works. It's a pretty essential part of Haskell, so it is certainly going in.

#4 Would be quite difficult. I probably wouldn't be able to include this. Instead I will require explicit type annotations on functions.

#5 Definitely want to include this. Should be pretty simple.

#6 Not sure about this. Will definitely require a fair bit of research on my part. It's an important part of Haskell, but I honestly have no idea how it works. It seems really cool, so I'd really like to include it.

Since my formal background in programming languages is about nil, I've slotted myself a fair bit of reading. So far today I've humped through the first 11 chapters of Types and Programming Languages. I'm not the biggest fan of the way the book goes about things, but it's not bad.