Program extraction from proofs using classical dependent choice

Add to your list(s) Download to your calendar using vCal

• Monika Seisenberger, University of Swansea
• Thursday 22 July 2010, 10:00-11:00
• 217 Computer Science.

If you have a question about this talk, please contact Paul Levy.

In this talk I begin with a short introduction and demonstration of program extraction from proofs in the interactive theorem prover Minlog. Then I will report about examples of programs extracted from classical proofs, in particular from proofs using classical dependent choice, and discuss their efficiency.

This talk is part of the Theoretical computer science seminar series.

This talk is included in these lists:

• 217 Computer Science
• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• Theoretical computer science seminar
• computer sience

Note that ex-directory lists are not shown.