Introduction

Optional module g5bcfr is based on the remarkable fact that in a strong sense, mathematical proof is functional programming in disguise! We'll be peeling away that disguise and showing how you can integrate programming and proof in a single system, if you happen to have a functional language with an expressive type system handy...

...and you do! Under your very noses, in fact. The Epigram programming language (http://www.e-pig.org/) and its interactive (colour!) editor are being developed right here in Nottingham, and this course is brought to you by some of the team who are working on the system and the issues it addresses.

Writing provably correct programs can be clean, can be neat, can be easy and can be seriously addictive. Hacking has never been so exact. Try it.

What's when?

  • Lectures are on Tuesdays at 3pm and Thursdays at 10am in room C1, the Exchange.
  • Labs will be one hour per week, probably on Wednesday morning.
  • Cookies are available without obligation at the first lecture, on 3 October 2006.

Who's who?

Reading

  • The Epigram website is a good place to get hold of the system, as well as much reading material.
  • The manual is indispensable.
  • These lecture notes from Advanced Functional Programming 2004 (an international summer school held in Tartu, Estonia) provide relevant background reading and exercises, some quite, er, advanced.
  • 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.