Abstract
During the first week of July 1995 I visited SRI Menlo Park to find
out more about PVS (Prototype Verification System). The
preceding week I attended LICS95, where I had several talks with
Natarajan Shankar accompanied by demos of the system on his SparcBook
laptop.
This note consists of a somewhat rambling and selective report on some
of the things I learned, together with a discussion of their implications
for the evolution of the HOL system.
compressed postscript (75K)