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

Publikation: Bidrag til tidsskrift › Tidsskriftartikel › Forskning › fagfællebedømt

Standard

Admissible Types-to-PERs Relativization in Higher-Order Logic. / Popescu, Andrei; Traytel, Dmitriy.

I: Proceedings of the ACM on Programming Languages, Bind 7, Nr. POPL, 42, 2023.

Publikation: Bidrag til tidsskrift › Tidsskriftartikel › Forskning › fagfællebedømt

Harvard

Popescu, A & Traytel, D 2023, 'Admissible Types-to-PERs Relativization in Higher-Order Logic', Proceedings of the ACM on Programming Languages, bind 7, nr. POPL, 42. https://doi.org/10.1145/3571235

APA

Popescu, A., & Traytel, D. (2023). Admissible Types-to-PERs Relativization in Higher-Order Logic. Proceedings of the ACM on Programming Languages, 7(POPL), [42]. https://doi.org/10.1145/3571235

Vancouver

Popescu A, Traytel D. Admissible Types-to-PERs Relativization in Higher-Order Logic. Proceedings of the ACM on Programming Languages. 2023;7(POPL). 42. https://doi.org/10.1145/3571235

Author

Popescu, Andrei ; Traytel, Dmitriy. / Admissible Types-to-PERs Relativization in Higher-Order Logic. I: Proceedings of the ACM on Programming Languages. 2023 ; Bind 7, Nr. POPL.

Bibtex

@article{1fb8d52e5c884079987f29f7fd01dc90,
title = "Admissible Types-to-PERs Relativization in Higher-Order Logic",
abstract = "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. ",
keywords = "Higher-order logic (HOL), Interactive theorem proving, Isabelle/HOL, Partial equivalence relation, Proof theory, Relativization, Type definition",
author = "Andrei Popescu and Dmitriy Traytel",
note = "Publisher Copyright: {\textcopyright} 2023 Owner/Author.",
year = "2023",
doi = "10.1145/3571235",
language = "English",
volume = "7",
journal = "Proceedings of the ACM on Programming Languages",
issn = "2475-1421",
publisher = "ACM",
number = "POPL",

}

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