Our paper “Polymorphism Meets DHOL” by Rhea Ranalter, Florian Rabe, and Cezary Kaliszyk has been officially published as part of LIPIcs, Volume 378, FSCD'26.
DHOL (Dependent Higher-Order Logic) is a powerful logic with dependent types and strong ATP support. This paper develops polymorphic DHOL (PDHOL), extending the expressivity of DHOL while retaining its simple definition and automation, with a sound and complete translation to polymorphic HOL implemented in a logic-embedding tool.
[Read More]