Polymorphism Meets DHOL
Ranalter R, Rabe F, Kaliszyk C (2026)
Publication Type: Conference contribution
Publication year: 2026
Journal
Publisher: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Book Volume: 378
Conference Proceedings Title: Leibniz International Proceedings in Informatics, LIPIcs
Event location: Lisbon
ISBN: 9783959774338
DOI: 10.4230/LIPIcs.FSCD.2026.27
Abstract
DHOL is an extensional, classical logic that equips the well-known higher-order logic (HOL) with dependent types. This allows for concise encodings of important domains like size-bounded data structures, category theory, or proof theory. Automation support is obtained by translating DHOL to HOL, for which powerful modern automated theorem provers are available. However, a critically missing feature of DHOL is polymorphism. We develop the syntax and semantics of polymorphic DHOL and extend the translation accordingly. We implement the translation in the logic-embedding tool and evaluate it on a range of TPTP formalizations. The logic-embedding tool, together with an off-the-shelf HOL theorem prover easily creates a PDHOL theorem prover for experimenting.
Authors with CRIS profile
Involved external institutions
Austria (AT)How to cite
APA:
Ranalter, R., Rabe, F., & Kaliszyk, C. (2026). Polymorphism Meets DHOL. In Frank Pfenning (Eds.), Leibniz International Proceedings in Informatics, LIPIcs. Lisbon, PT: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing.
MLA:
Ranalter, Rhea, Florian Rabe, and Cezary Kaliszyk. "Polymorphism Meets DHOL." Proceedings of the 11th International Conference on Formal Structures for Computation and Deduction, FSCD 2026, Lisbon Ed. Frank Pfenning, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2026.
BibTeX: Download