Monika Seisenberger: Programs from constructive and classical proofs

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.

Leave a Reply

Your email address will not be published. Required fields are marked *

Time limit is exhausted. Please reload CAPTCHA.