Abstract

Users of interactive theorem provers based on Higher-Order Logic (such as HOL4 , HOL Light and Isabelle/HOL) find it very convenient to “ride” the HOL type system when defining concepts and reasoning about them— within a paradigm that can be called type-based reasoning. However, to achieve higher flexibility, users often need to resort to set-based reasoning, which is more bureaucratic and less supported by automation. In previous work with Ondrej Kuncar, I developed a mechanism called Types-to-Sets that allows one to have the best of both worlds by offering a bridge between the simpler type-based theorems and the heavier set-based ones. In recent work jointly with Dmitriy Traytel I show that, contrary to the previous belief, the rules for moving from types to sets are admissible in the standard Higher-Order Logic used in theorem provers, so no extension of the axiomatization base is required. In this talk, I will motivate and introduce the Types-to-Sets framework, and will present our recent admissibility result and its connection to other concepts such as Reynolds-style parametricity and compositional (co)datatypes. (Joint work Ondrej Kuncar and Dmitriy Traytel)