University of Birmingham > Talks@bham > Theoretical computer science seminar > Program extraction from proofs using classical dependent choice

Program extraction from proofs using classical dependent choice

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

  • UserMonika Seisenberger, University of Swansea
  • ClockThursday 22 July 2010, 10:00-11:00
  • House217 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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on from the University of Cambridge.