Admissible Types-to-PERs Relativization in Higher-Order Logic
Research output: Contribution to journal › Journal article › Research › peer-review
Standard
Admissible Types-to-PERs Relativization in Higher-Order Logic. / Popescu, Andrei; Traytel, Dmitriy.
In: Proceedings of the ACM on Programming Languages, Vol. 7, No. POPL, 42, 2023.Research output: Contribution to journal › Journal article › Research › peer-review
Harvard
APA
Vancouver
Author
Bibtex
}
RIS
TY - JOUR
T1 - Admissible Types-to-PERs Relativization in Higher-Order Logic
AU - Popescu, Andrei
AU - Traytel, Dmitriy
N1 - Publisher Copyright: © 2023 Owner/Author.
PY - 2023
Y1 - 2023
N2 - 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.
AB - 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.
KW - Higher-order logic (HOL)
KW - Interactive theorem proving
KW - Isabelle/HOL
KW - Partial equivalence relation
KW - Proof theory
KW - Relativization
KW - Type definition
UR - http://www.scopus.com/inward/record.url?scp=85146578874&partnerID=8YFLogxK
U2 - 10.1145/3571235
DO - 10.1145/3571235
M3 - Journal article
AN - SCOPUS:85146578874
VL - 7
JO - Proceedings of the ACM on Programming Languages
JF - Proceedings of the ACM on Programming Languages
SN - 2475-1421
IS - POPL
M1 - 42
ER -
ID: 335694002