Compact Course "Program Extraction"

January 30, 2020

Notice that the timetable has changed!
NEW: links to course material added below

The minicourse “Program Extraction” by Monika Seisenberger will be held on-line from 25th to 29th May 2020.

Registration will be required by 25nd May 18:00. To register please send an email to Franziskus Wiesnet.

Program Extraction
Monika Seisenberger (Swansea University)

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

Timetable
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-16:00

The course will be completed by the seminar talk Logic in Railway Verification on Friday, May 29 at 16:00-17:00.

Course material - course slides - minlog system - minlog tutorial