Notes on PVS from a HOL perspective

Michael J.C. Gordon
Reader in Formal Methods
University of Cambridge Computer Laboratory
New Museums Site, Pembroke Street
CAMBRIDGE CB2 3QG, United Kingdom.
work: (+44) 1223 334627, fax: (+44) 1223 334678, home: (+44) 1223 362123

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)