Tuesday, February 28, 2017, 15.00
Howard House 4th Floor Seminar Room
Speaker: Monika Seisenberger (Swansea University)
Title: Programs from constructive and classical proofs
Program extraction from formal proofs is a powerful proof theoretic technique based on realisability to obtain provably correct programs. In this talk we give a short overview on the state-of-the-art, give several examples for program extraction from constructive proofs in different areas (Well-quasiorders, Sat Solving, Parsing), and also show how classical proofs which are often more concise and elegant compared to a constructive counterpart can lead to interesting programs. The case studies are carried out in the interactive theorem prover Minlog.