Logic and Set Theory: Programs from constructive and classical proofs

28 February 2017, 3.00 PM - 28 February 2017, 4.30 PM

Monika Seisenberger (Swansea)

Howard House 4th Floor Seminar Room

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.

Contact information

Philip Welch

Edit this page