Abstract: Logic and Type Theory in Theorem Provers
Jonathan P. Seldin
This talk will be a discussion of the conditions for a theorem prover or
proof assistant to be both useful and trusted. The emphasis will be on the
relationship between systems based on the calculus of constructions and HOL.