BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:A tutorial introduction to the PVS proof assistant - Natarajan Sha
 nkar (SRI International)
DTSTART:20170630T090000Z
DTEND:20170630T100000Z
UID:TALK73120@talks.cam.ac.uk
CONTACT:INI IT
DESCRIPTION:The Prototype Verification System (PVS) is an interactive proo
 f assistant developed at SRI International.&nbsp\; The PVS specification l
 anguage extends higher-order logic with predicate subtypes\, dependent typ
 es\, inductive datatypes\, and parametric theories.&nbsp\; These features 
 make typechecking undecidable\, or more accurately\, decidable modulo proo
 f obligations.&nbsp\; The interactive proof assistant includes automated s
 upport for contextual&nbsp\; simplification\, rewriting\, and SAT/SMT solv
 ing. PVS has been used to formalize large libraries (see\, for example\,&n
 bsp\; https://github.com/nasa/pvslib).&nbsp\;&nbsp\; The tutorial gives a 
 brief overview of the language\, logic\, and proof infrastructure of PVS.
LOCATION:Seminar Room 2\, Newton Institute
END:VEVENT
END:VCALENDAR