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.