Admissible Types-to-PERs Relativization in Higher-Order Logic
Publikation: Bidrag til tidsskrift › Tidsskriftartikel › Forskning › fagfællebedømt
Dokumenter
- Fulltext
Forlagets udgivne version, 401 KB, PDF-dokument
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.
Originalsprog | Engelsk |
---|---|
Artikelnummer | 42 |
Tidsskrift | Proceedings of the ACM on Programming Languages |
Vol/bind | 7 |
Udgave nummer | POPL |
Antal sider | 32 |
DOI | |
Status | Udgivet - 2023 |
Bibliografisk note
Publisher Copyright:
© 2023 Owner/Author.
ID: 335694002