Thu 19 Jan 2023 15:10 - 15:35 at Avenue34 - Type Theory Chair(s): Brigitte Pientka

Relativizing statements in Higher-Order Logic (HOL) from types to sets is useful for improving productivity when working with HOL-based interactive theorem provers such as HOL4, HOL Light and Isabelle/HOL. This paper provides the first comprehensive definition and study of types-to-sets relativization in HOL, done in the more general form of types-to-PERs (partial equivalence relations). We prove that, for a large practical fragment of HOL which includes container types such as datatypes and codatatypes, types-to-PERs relativization is admissible, in that the provability of the original, type-based statement implies the provability of its relativized, PER-based counterpart. Our results also imply the admissibility of a previously proposed axiomatic extension of HOL with local type definitions. We have implemented types-to-PERs relativization as an Isabelle tool that performs relativization of HOL theorems on demand.

Thu 19 Jan

Displayed time zone: Eastern Time (US & Canada) change

15:10 - 16:25
Type TheoryPOPL at Avenue34
Chair(s): Brigitte Pientka McGill University
15:10
25m
Talk
Admissible Types-to-PERs Relativization in Higher-Order LogicDistinguished Paper
POPL
Andrei Popescu University of Sheffield, Dmitriy Traytel University of Copenhagen
DOI
15:35
25m
Talk
An Order-Theoretic Analysis of Universe Polymorphism
POPL
Kuen-Bang Hou (Favonia) University of Minnesota, Carlo Angiuli Carnegie Mellon University, Reed Mullanix University of Minnesota
DOI
16:00
25m
Talk
Impredicative Observational Equality
POPL
DOI