Computer Aided Formal Reasoning (G53CFR)

Introduction

Optional module G53CFR is all about the remarkable correspondence between formal proof and functional programming, known as the Curry-Howard isomorphism. With an expressive enough type system one can provide proofs of correctness in the same language as the program we want to prove correct. This process can also change the way we think about the original program, and help us to install correctness from the very beginning of the programming process.

We aim to show that not only are these ideas useful, but programming and proving in this fashion is also be fun. You won't how much fun until you try it!

Lecture Notes

Such as they are:

• Lecture 3 Negation
• Lecture 5 Double Negation and Predicate Logic
• LangBroken.agda The first (broken) attempt at evaluating our small language
• LangMaybe.agda And the fix, using 'Maybe'

Exercises

Exercises consists largely of downloadable Agda files with holes which should be filled in. Get them here, when they're half cooked.

Submission is via the unix coursework submission system (cw-submit).

• Solution 1
• Solution 2
• Solution 3
• Solution 4
• Solution 5
• Solution 6
• Solution 7
• The final coursework Due 23/1/09, 13:30

There will be no more weekly courseworks or labs. Note that revising from courseworks 1-7 is highly recommended. If you want to download an original, change 'Sol' in the link for 'Sec'.

What's when?

• Lectures are on Mondays 10-11 Room B12, Amenities Building and Tuesdays 10-11 Room A07, Business School SOUTH.
• Labs are Wednesdays 10-11 Room B52, Computer Science. Note that this is the only lab with Agda installed!

Installing Agda

You might like to have Agda available on your own machine. This isn't necessarily that easy, but these are the things to try first:

• Windows users can try the Windows installer bear in mind that this can take a while, just be patient.
• Those with Debian based Linux distributions, including Ubuntu can try Liyang HU's Agda repository by following his instructions HERE.
• OSX users are not so lucky, you might have to do it by hand.

Discussion

Is encouraged, the appropriate forum is HERE!

Reading

• The Agda website is a good place to get hold of the system, as well as much reading material.
• This tutorial in particular, could be useful. It approaches the basics from a different perspective to this course.
• Why dependent types matter is a draft article by Thorsten Altenkirch, Conor McBride and James McKinna, aimed at functional programmers, trying to explain what we're on about. The language used is Epigram a prototype developed here in Nottingham that preceded the latest version of Agda.