Interactive Theorem Proving: The Isabelle Experience
Event details
| Date | 10.06.2014 |
| Hour | 11:15 |
| Speaker | Tobias NIPKOW, Technical University of Munich |
| Location | |
| Category | Conferences - Seminars |
The dream of machines that prove mathematical theorems automatically goes back to the beginning computer science. Meanwhile it has become a reality, although we had to replace "automatic" with "interactive" to make it work. Modern Interactive Theorem Provers (or Proof Assistants) are like programming environments, except that they help us write proofs instead of programs. Crucially, they check the proofs for logical correctness and (try to) bridge gaps in the argument by constructing missing subproofs automatically.
This talk will present an overview of the field from the perspective of the Isabelle proof assistant. I will talk about a range of applications from the proof of the Kepler Conjecture via the analysis of programming languages and operating systems to the role of proof assistants in teaching. A demo of the Isabelle systems will help the audience to get a feeling for what is involved when trying to convince a machine that some theorem is true.
This talk will present an overview of the field from the perspective of the Isabelle proof assistant. I will talk about a range of applications from the proof of the Kepler Conjecture via the analysis of programming languages and operating systems to the role of proof assistants in teaching. A demo of the Isabelle systems will help the audience to get a feeling for what is involved when trying to convince a machine that some theorem is true.
Links
Practical information
- General public
- Free
Organizer
- Viktor Kuncak
Contact
- Sylvie Thomet