How to prove a theorem using the Isabelle Proof Assistant

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

• John Wickerson (Imperial College)
• Monday 22 January 2018, 16:00-17:00
• Level 9 Seminar Room, EE Dept..

If you have a question about this talk, please contact George A Constantinides.

I will give an interactive demonstration of how the Isabelle Proof Assistant (https://isabelle.in.tum.de/) can be used to build computer-checked proofs of a few simple theorems. We will look at the “procedural” style of proof, where a proof is given as a sequence of procedures to apply, and also at the more modern “declarative” style, where a proof looks more like how a mathematician would write it.

This talk is part of the CAS Talks series.

This talk is included in these lists:

• Andrea Picciau's list
• CAS Talks
• Circuits and Systems Group: Internal Seminars
• Level 9 Seminar Room, EE Dept.

Note that ex-directory lists are not shown.