Minicorso "Program Extraction" by Monika Seisenberger

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

Registration will be required by 22nd May. To register please send an email to Franziskus Wiesnet: franziskus.wiesnet(at)unitn.it

Timetable and Zoom site will be made available in due time at the course web site:

                                        http://www.di.univr.it/?ent=seminario&id=5081&idC=70

Program of the course:

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