BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Types-To-Sets and Types-to-PERs Relativization in Higher-Order Log
 ic - Andrei Popescu\, University of Sheffield
DTSTART:20230505T130000Z
DTEND:20230505T140000Z
UID:TALK197887@talks.cam.ac.uk
CONTACT:Jamie Vicary
DESCRIPTION:Users of interactive theorem provers based on Higher-Order Log
 ic (such\nas HOL4\, HOL Light and Isabelle/HOL) find it very convenient to
  "ride"\nthe HOL type system when defining concepts and reasoning about th
 em --\nwithin a paradigm that can be called *type-based reasoning*. Howeve
 r\,\nto achieve higher flexibility\, users often need to resort to\n*set-b
 ased reasoning*\, which is more bureaucratic and less supported\nby automa
 tion. In previous work with Ondrej Kuncar\, I developed a\nmechanism calle
 d Types-to-Sets that allows one to have the best of\nboth worlds by offeri
 ng a bridge between the simpler type-based\ntheorems and the heavier set-b
 ased ones. In recent work jointly with\nDmitriy Traytel I show that\, cont
 rary to the previous belief\, the\nrules for moving from types to sets are
  admissible in the standard\nHigher-Order Logic used in theorem provers\, 
 so no extension of the\naxiomatization base is required. In this talk\, I 
 will motivate and\nintroduce the Types-to-Sets framework\, and will presen
 t our recent\nadmissibility result and its connection to other concepts su
 ch as\nReynolds-style parametricity and compositional (co)datatypes. (Join
 t work Ondrej Kuncar and Dmitriy Traytel)
LOCATION:SS03\, Computer Laboratory
END:VEVENT
END:VCALENDAR