Compact Course "Program Extraction"
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.
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
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