Program Extraction [1 ECTS Mat/01]

Speaker:  Monika Seisenberger - Swansea University
  Tuesday, May 26, 2020 at 8:30 AM 26-29 May, on-line
The course will be held on-line. Please register by writing an email to Franziskus Wiesnet: franziskus.wiesnet(at)

Part 1 Extraction of Programs from Constructive Proofs
1.1 Introduction, Curry Howard-Correspondence, Realizability Interpretation
1.2 Tool Support, Examples, Extension to Inductive Definitions
Part 2 Extraction of Programs from Classical Proofs
2.1 A-Translation, Choice principles
2.2 Applications for Both Parts

Tuesday, May 26: 8:40-10:20
Wednesday, May 27: 8:40-10:20
Thursday, May 28: 8:40-10:20
Friday, May 29: 15.00-17:00 of which the second hour as department seminar.

Monika Seisenberger's profile:


Programme Director
Peter Michael Schuster

External reference
Publication date
January 29, 2020