Admissible Types-to-PERs Relativization in Higher-Order Logic

Research output: Contribution to journalJournal articleResearchpeer-review

Documents

  • Fulltext

    Final published version, 401 KB, PDF document

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.

Original languageEnglish
Article number42
JournalProceedings of the ACM on Programming Languages
Volume7
Issue numberPOPL
Number of pages32
DOIs
Publication statusPublished - 2023

Bibliographical note

Publisher Copyright:
© 2023 Owner/Author.

    Research areas

  • Higher-order logic (HOL), Interactive theorem proving, Isabelle/HOL, Partial equivalence relation, Proof theory, Relativization, Type definition

ID: 335694002