Types in Higher-Order Logic (HOL) are naturally interpreted as nonempty sets—this intuition is reflected in the type definition rule for the HOL-based systems (including Isabelle/HOL), where a new type can be defined whenever a nonempty set is exhibited. However, in HOL this definition mechanism cannot be applied inside proof contexts. We propose a more expressive type definition rule that addresses the limitation and we prove its soundness. This higher expressive power opens the opportunity for a HOL tool that relativizes type-based statements to more flexible set-based variants in a principled way. We also address particularities of Isabelle/HOL and show how to perform the relativization in the presence of type classes.
CITATION STYLE
Kunčar, O., & Popescu, A. (2016). From types to sets by local type definitions in higher-order logic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9807 LNCS, pp. 200–218). Springer Verlag. https://doi.org/10.1007/978-3-319-43144-4_13
Mendeley helps you to discover research relevant for your work.