Proofs-as-programs correspondence, recent developments and type isomorphisms (5 ECTS)Objectives of the courseAfter 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 programmeHomework exercises done.
PrerequisitesFamiliarity with functional programming or mathematical proofs would be beneficial. |