Types-To-Sets and Types-to-PERs Relativization in Higher-Order Logic

Add to your list(s) Download to your calendar using vCal

• Andrei Popescu, University of Sheffield
• Friday 05 May 2023, 14:00-15:00
• SS03, Computer Laboratory.

If you have a question about this talk, please contact Jamie Vicary.

Users of interactive theorem provers based on Higher-Order Logic (such as HOL4 , HOL Light and Isabelle/HOL) find it very convenient to “ride” the HOL type system when defining concepts and reasoning about them— within a paradigm that can be called type-based reasoning. However, to achieve higher flexibility, users often need to resort to set-based reasoning, which is more bureaucratic and less supported by automation. In previous work with Ondrej Kuncar, I developed a mechanism called Types-to-Sets that allows one to have the best of both worlds by offering a bridge between the simpler type-based theorems and the heavier set-based ones. In recent work jointly with Dmitriy Traytel I show that, contrary to the previous belief, the rules for moving from types to sets are admissible in the standard Higher-Order Logic used in theorem provers, so no extension of the axiomatization base is required. In this talk, I will motivate and introduce the Types-to-Sets framework, and will present our recent admissibility result and its connection to other concepts such as Reynolds-style parametricity and compositional (co)datatypes. (Joint work Ondrej Kuncar and Dmitriy Traytel)

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• SS03, Computer Laboratory
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• tcw57’s list
• yk373's list

Note that ex-directory lists are not shown.