Teaching Theorem Proving in Agda: What Already Exists?

I’m not shy in my love of constructive mathematics and theorem proving in type theory. My first theorem prover was Coq and at some point I was decently good with Isabelle/HOL, but my current technology of choice is probably Agda. This is less of a judgment about what’s The Best Tool and more that I find it fits my brain better. I think of myself as only being an intermmediate Agda user, though, because there’s plenty of features and topics I don’t have that much experience with. I’ve done a lot of bits of toy code, but not a lot of complicated things. I want to learn even more and maybe get to be more of an expert, and the best way I learn any topic is to try and teach it!

In a perfect world, I’d have the opportunity to teach a course about programming/proving in Agda, but it’s unlikely that will be an undergraduate or even graduate course at my institution at any point before I’m gone from here. On the other hand, one doesn’t actually need to be getting paid to teach in order to write introductory or even advanced materials on the topic.

That being said, I was thinking that I might try to start writing tutorial material in order to improve my understanding of Agda. Looking through some of the materials linked at http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Othertutorials it looks like most of what’s out there is a really really basic introduction, but there’s not a lot that shows things like “here’s times to use setoids” or “here’s how you use equational reasoning”. The closest thing I’ve seen out there is http://oxij.org/note/BrutalDepTypes/, but I think there could be something even more extensive that could be useful.

Because I’m me I feel like it’s the height of arrogance that I’d want to write something like this, but maybe it’ll actually get me more involved in the community and asking questions rather than watching silently from the shadows, like a creeper.

Any thoughts?

About these ads

2 thoughts on “Teaching Theorem Proving in Agda: What Already Exists?

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