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