Logic and Set Theory: Programs from constructive and classical proofs
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.