Admissible Types-to-PERs Relativization in Higher-Order Logic
Research output: Contribution to journal › Journal article › Research › peer-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 language | English |
---|---|
Article number | 42 |
Journal | Proceedings of the ACM on Programming Languages |
Volume | 7 |
Issue number | POPL |
Number of pages | 32 |
DOIs | |
Publication status | Published - 2023 |
Bibliographical note
Publisher Copyright:
© 2023 Owner/Author.
- Higher-order logic (HOL), Interactive theorem proving, Isabelle/HOL, Partial equivalence relation, Proof theory, Relativization, Type definition
Research areas
ID: 335694002