The HOL theorem-proving system

I will introduce the HOL system, first giving a high-level description of its general capabilities, and then focussing on some of the details of its implementation. The latter part of the talk will stress the simplicity of the kernel's API and discuss some alternative implementation strategies, with a view to demonstrating that the HOL system is a great base for experimentation. I will close by talking about some recent applications using HOL.

Micheal Norrish
Michael Norrish is a post-doctoral research fellow in the Logic and Computation Programme of NICTA.

Date:Wed Sep 8 2004
Time: 10:30am to 12:00pm
Location: G3, Electrical Engineering (UNSW)
RSISE Video Conference Room; A207, building 115, cnr. North and Daley Roads (ANU)

Return to index


Last updated by rhuuck at Fri Sep 3 13:29:49 2004 GMT+1000