Software Foundations in Isabelle

So I’m guessing that many of my readers are going to be familiar with Pierce et al.’s book Software Foundations, which is essentially a retelling of chunks of Pierce’s Types and Programming Languages book that also teaches the proof-assistant Coq at the same time. It’s a good book and the way I first learned Coq. So, about 4 years ago, when I was first learning the proof-assistant Isabelle/HOL I converted the then-current version of Software Foundations from Coq to Isabelle. I’ve decided to make that old version available on github here. To those well versed in Isabelle, it will probably seem a bit naive I fear, but that’s because this was how I learned the theorem prover in the first place. Some of my deep-seated fear makes it very very difficult to ask questions, so I essentially just taught myself through trial, error, and looking at other code developments.

The format is also a little messy at the moment in that most of the original explanatory text and Coq code is still in-line with the Isabelle code and explanations, mostly because that’s how I actually wrote all the Isabelle code for it originally and I liked having the Coq and Isabelle side-by-side.

If there’s any interest in developing it further or adapting it to more recent versions of Software Foundations, I’d be more than happy to start maintaining it again. It just seemed, after all this time, I should actually let this old project see the light of day.

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s