Certified Programming - A taste of interactive theorem proving
Daniel James ( OUCL )
- 16:00 13th February 2009 ( week 4, Hilary Term 2009 )479
Research into automated and interactive theorem proving has gone on
for many decades, dating back to early projects such as Automath in
the late 60's. In this talk I will give an introduction to one such
system, called Coq. 25 years after its inception, Coq is now a mature
and stable tool for developing certified programs. I will cover the
key features of Coq and provide a taste for the practical use of the
tool with a live demonstration.
Share this:
