DROPS

Document

DOI: 10.4230/LIPIcs.FSCD.2026.27

Polymorphism Meets DHOL

Authors: Rhea Ranalter, Florian Rabe, and Cezary Kaliszyk

Published in: LIPIcs, Volume 378, 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)

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.

Cite as

Rhea Ranalter, Florian Rabe, and Cezary Kaliszyk. Polymorphism Meets DHOL. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 27:1-27:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{ranalter_et_al:LIPIcs.FSCD.2026.27,
  author =	{Ranalter, Rhea and Rabe, Florian and Kaliszyk, Cezary},
  title =	{{Polymorphism Meets DHOL}},
  booktitle =	{11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
  pages =	{27:1--27:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-433-8},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{378},
  editor =	{Pfenning, Frank},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.27},
  URN =		{urn:nbn:de:0030-drops-263774},
  doi =		{10.4230/LIPIcs.FSCD.2026.27},
  annote =	{Keywords: Polymorphism, Dependent Types, Higher-order Logic, Automated Reasoning}
}

Search Results

Documents authored by Ranalter, Rhea

Polymorphism Meets DHOL

Abstract

Cite as

Thanks for your feedback!

Could not send message