Admissible Types-to-PERs Relativization in Higher-Order Logic
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 JanDisplayed time zone: Eastern Time (US & Canada) change
15:10 - 16:25
|Admissible Types-to-PERs Relativization in Higher-Order LogicDistinguished Paper
|An Order-Theoretic Analysis of Universe Polymorphism
Kuen-Bang Hou (Favonia) University of Minnesota, Carlo Angiuli Carnegie Mellon University, Reed Mullanix University of MinnesotaDOI
|Impredicative Observational Equality