Teaching‎ > ‎Aarhus Mini-course‎ > ‎

Description

Proofs-as-programs correspondence, recent developments and type isomorphisms (5 ECTS)

Objectives of the course

After introducing the classic Curry-Howard correspondence between mathematical proofs and computer programs, the student will become acquainted with the newer extensions of the correspondence to control and delimited control operators. The Agda proof assistant software that implements this correspondence will be used to give the student some hands-on experience in building formal proofs. This technology will be used, in particular, for reflecting upon the correspondence itself: it will be shown how to use it to build certified normalization-by-evaluation proofs/programs. Finally, type isomorphisms and the sum isomorphism problem will be explained.

To the non-specialist student, this course should give usable beginning knowledge to proofs-as-programs: the application area is wide: from certification of computer programs to applications to foundations of Mathematics. To specialist students, the application of Agda to normalization-by-evaluation will be new, and also they may profit from the presentation of new and open problems like sum isomorphisms or constructive logical systems for delimited control.

Learning outcomes and competences

At the end of the course the student should be able to:

  • understand how proofs and programs are one and the same thing, including recent extensions
  • use Agda or any other proof assistant based on type theory
  • understand some open problems in this area

Compulsory programme

Homework exercises done.

Prerequisites

Familiarity with functional programming or mathematical proofs would be beneficial.
Comments