Abstract for invited tutorial given at the TPHOLs (Theorem Proving in Higher-Order Logics) '96 International Conference in Turku, Finland, August 1996.

This 90min tutorial covered two of the more novel aspects of the Nuprl and PVS theorem provers:
Expressive type systems.
These make specifications more consise and accurate, but good automation is needed to solve proof obligations that arise during type-checking.
Support for abstract theories.
These have uses in supporting mechanical proof developments, and in the domains of program specification refinement and mathematics. Key issues are whether types can be formed for classes of abstract theories and the need for automatic inference of theory interpretations.

The tutorial assumed some familiarity with HOL-like theorem provers, but did not assume familiarity with either PVS or Nuprl in particular. The issue of Nuprl's constructivity was orthogonal to the issues discussed and was therefore glossed over.

Last Modified Sept 17th, 1996