BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:Interactive Theorem Proving: The Isabelle Experience
DTSTART:20140610T111500
DTSTAMP:20260407T021037Z
UID:cbfdf41d14ae2c16cc874beed6223c18161685bd991ad0cdf4c7f441
CATEGORIES:Conferences - Seminars
DESCRIPTION:Tobias NIPKOW\, Technical University of Munich\nThe dream of m
 achines that prove mathematical theorems automatically goes back to the be
 ginning computer science. Meanwhile it has become a reality\, although we 
 had to replace "automatic" with "interactive" to make it work. Modern Inte
 ractive Theorem Provers (or Proof Assistants) are like programming environ
 ments\, except that they help us write proofs instead of programs. Crucial
 ly\, they check the proofs for logical correctness and (try to) bridge gap
 s in the argument by constructing missing subproofs automatically.\nThis t
 alk will present an overview of the field from the perspective of the Isab
 elle proof assistant. I will talk about a range of applications from the p
 roof of the Kepler Conjecture via the analysis of programming languages an
 d 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.
LOCATION:BC 420 https://plan.epfl.ch/?room==BC%20420
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR