Document Open Access Logo

Polymorphism Meets DHOL

Authors Rhea Ranalter , Florian Rabe , Cezary Kaliszyk

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2026.27.pdf
  • Filesize: 0.78 MB
  • 21 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Automated reasoning
  • Theory of computation → Higher order logic
  • Theory of computation → Type theory
Keywords
  • Polymorphism
  • Dependent Types
  • Higher-order Logic
  • Automated Reasoning

Metrics

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 Get BibTex

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) https://doi.org/10.4230/LIPIcs.FSCD.2026.27

Author Details

Rhea Ranalter
  • University of Innsbruck, Computational Logic, Austria
Florian Rabe
  • University of Erlangen-Nuremberg, Computer Science, Germany
Cezary Kaliszyk
  • University of Melbourne, School of Computing and Information Systems, Australia
  • University of Innsbruck, Computational Logic, Austria

Funding

Rabe was supported by the FAUstairs project (see https://www.faustairs.fau.de/), funded by the Stiftung Innovation in der Hochschullehre under grant StIL:1001-3096. Kaliszyk and Ranalter were supported by the Renaissance Philanthropy grant DEEPER.

Acknowledgements

We want to thank Alexander Steen for his work on the logic-embedding tool, which allowed for effective integration of our translation.

Supplementary Materials

References

  1. S. Allen. A Non-Type-Theoretic Semantics for Type-Theoretic Language. PhD thesis, Cornell University, 1987. Google Scholar
  2. P. Andrews. An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Academic Press, 1986. Google Scholar
  3. Jean-Philippe Bernardy, Patrik Jansson, and Ross Paterson. Parametricity and dependent types. In Paul Hudak and Stephanie Weirich, editors, Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010, pages 345-356. ACM, 2010. URL: https://doi.org/10.1145/1863543.1863592.
  4. A. Bhayat and G. Reger. A polymorphic vampire - (short paper). In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part II, volume 12167 of Lecture Notes in Computer Science, pages 361-368. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51054-1_21.
  5. A. Church. A Formulation of the Simple Theory of Types. Journal of Symbolic Logic, 5(1):56-68, 1940. URL: https://doi.org/10.2307/2266170.
  6. Coq Development Team. The Coq Proof Assistant: Reference Manual. Technical report, INRIA, 2015. Google Scholar
  7. Simon Cruanes. Extending Superposition with Integer Arithmetic, Structural Induction, and Beyond. (Extensions de la Superposition pour l'Arithmétique Linéaire Entière, l'Induction Structurelle, et bien plus encore). PhD thesis, École Polytechnique, Palaiseau, France, 2015. URL: https://tel.archives-ouvertes.fr/tel-01223502.
  8. Lukasz Czajka and Cezary Kaliszyk. Hammer for coq: Automation for dependent type theory. J. Autom. Reason., 61(1-4):423-453, 2018. URL: https://doi.org/10.1007/S10817-018-9458-4.
  9. L. de Moura, S. Kong, J. Avigad, F. van Doorn, and J. von Raumer. The Lean Theorem Prover (System Description). In A. Felty and A. Middeldorp, editors, Automated Deduction, pages 378-388. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-21401-6_26.
  10. Amy P. Felty and Dale Miller. Encoding a dependent-type lambda-calculus in a logic programming language. In Mark E. Stickel, editor, 10th International Conference on Automated Deduction, Kaiserslautern, FRG, July 24-27, 1990, Proceedings, volume 449 of Lecture Notes in Computer Science, pages 221-235. Springer, 1990. URL: https://doi.org/10.1007/3-540-52885-7_90.
  11. M. Gordon. HOL: A Proof Generating System for Higher-Order Logic. In G. Birtwistle and P. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis, pages 73-128. Kluwer-Academic Publishers, 1988. Google Scholar
  12. M. Gordon and A. Pitts. The HOL Logic. In M. Gordon and T. Melham, editors, Introduction to HOL, Part III, pages 191-232. Cambridge University Press, 1993. Google Scholar
  13. J. Harrison. HOL Light: A Tutorial Introduction. In Proceedings of the First International Conference on Formal Methods in Computer-Aided Design, pages 265-269. Springer, 1996. URL: https://doi.org/10.1007/BFB0031814.
  14. M. Hofmann. Extensional Constructs in Intensional Type Theory. CPHC/BCS distinguished dissertations. Springer, 1997. Google Scholar
  15. B. Jacobs and T. Melham. Translating dependent type theory into higher order logic. In M. Bezem and J. Groote, editors, Typed Lambda Calculi and Applications, pages 209-29, 1993. Google Scholar
  16. P. Martin-Löf. An Intuitionistic Theory of Types: Predicative Part. In Proceedings of the '73 Logic Colloquium, pages 73-118. North-Holland, 1974. Google Scholar
  17. J. Niederhauser, C. E. Brown, and C. Kaliszyk. Tableaux for automated reasoning in dependently-typed higher-order logic. In Christoph Benzmüller, Marijn J. H. Heule, and Renate A. Schmidt, editors, Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part I, volume 14739 of Lecture Notes in Computer Science, pages 86-104. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-63498-7_6.
  18. T. Nipkow, L. Paulson, and M. Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic. Springer, 2002. Google Scholar
  19. U. Norell. The Agda WiKi, 2005. URL: http://wiki.portal.chalmers.se/agda.
  20. S. Owre, J. Rushby, and N. Shankar. PVS: A Prototype Verification System. In D. Kapur, editor, 11th International Conference on Automated Deduction (CADE), pages 748-752. Springer, 1992. URL: https://doi.org/10.1007/3-540-55602-8_217.
  21. Andrei Popescu and Dmitriy Traytel. Admissible types-to-pers relativization in higher-order logic. In A. Ahmed, R. Findler, D. Garg, and F. Pottier, editors, Principles of Programming Languages, pages 1214-1245. ACM, 2023. URL: https://doi.org/10.1145/3571235.
  22. F. Rabe. Semantics for Dependently-Typed HOL. In A. Biere, C. Lutz, and S. Negri, editors, Automated Reasoning. Springer, 2026. to appear. Google Scholar
  23. Vincent Rahli, Mark Bickford, and Abhishek Anand. Formal program optimization in Nuprl using computational equivalence and partial types. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors, Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings, volume 7998 of Lecture Notes in Computer Science, pages 261-278. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39634-2_20.
  24. D. Ranalter, C. E. Brown, and C. Kaliszyk. Experiments with choice in dependently-typed higher-order logic. In Nikolaj S. Bjørner, Marijn Heule, and Andrei Voronkov, editors, LPAR 2024: Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning, Port Louis, Mauritius, May 26-31, 2024, volume 100 of EPiC Series in Computing, pages 311-320. EasyChair, 2024. URL: https://doi.org/10.29007/2V8H.
  25. Daniel Ranalter, Cezary Kaliszyk, Florian Rabe, and Geoff Sutcliffe. The dependently typed higher-order form for the TPTP world. In René Thiemann and Christoph Weidenbach, editors, Frontiers of Combining Systems - 15th International Symposium, FroCoS 2025, Reykjavik, Iceland, September 29 - October 1, 2025, Proceedings, volume 15979 of Lecture Notes in Computer Science, pages 287-305. Springer, 2025. URL: https://doi.org/10.1007/978-3-032-04167-8_16.
  26. A. Riazanov and A. Voronkov. The design and implementation of Vampire. AI Communications, 15:91-110, 2002. URL: http://content.iospress.com/articles/ai-communications/aic259.
  27. C. Rothgang and F. Rabe. Subtyping in dependently-typed higher-order logic. In R. Thiemann and C. Weidenbach, editors, Frontiers of Combining Systems - 15th International Symposium, FroCoS 2025, Reykjavik, Iceland, September 29 - October 1, 2025, Proceedings, volume 15979 of Lecture Notes in Computer Science, pages 98-114. Springer, 2025. URL: https://doi.org/10.1007/978-3-032-04167-8_6.
  28. C. Rothgang, F. Rabe, and C. Benzmüller. Theorem Proving in Dependently Typed Higher-Order Logic. In B. Pientka and C. Tinelli, editors, Automated Dedution, pages 438-455. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-38499-8_25.
  29. C. Rothgang, F. Rabe, and C. Benzmüller. Dependently-Typed Higher-Order Logic. ACM Transactions on Computational Logic, 27(1), 2025. Google Scholar
  30. M. Southern. A Framework for Reasoning about LF Specifications. PhD thesis, University of Minnesota, 2021. Google Scholar
  31. A. Steen. An extensible logic embedding tool for lightweight non-classical reasoning (short paper). In B. Konev, C. Schon, and A. Steen, editors, Practical Aspects of Automated Reasoning, volume 3201 of CEUR Workshop Proceedings. CEUR-WS.org, 2022. URL: https://ceur-ws.org/Vol-3201/paper13.pdf.
  32. A. Steen and C. Benzmüller. The higher-order prover Leo-III. In G. De Giacomo, A. Catalá, B. Dilkina, M. Milano, S. Barro, A. Bugarín, and J. Lang, editors, European Conference on Artificial Intelligence, pages 2937-2938. IOS Press, 2020. URL: https://doi.org/10.3233/FAIA200462.
  33. A. Steen, M. Wisniewski, and C. Benzmüller. Going polymorphic - th1 reasoning for leo-iii. In Thomas Eiter, David Sands, Geoff Sutcliffe, and Andrei Voronkov, editors, IWIL Workshop and LPAR Short Presentations, volume 1 of Kalpa Publications in Computing, pages 100-112. EasyChair, 2017. URL: https://doi.org/10.29007/jgkw.
  34. P. Vukmirovic, A. Bentkamp, J. Blanchette, S. Cruanes, V. Nummelin, and S. Tourret. Making higher-order superposition work. J. Autom. Reason., 66(4):541-564, 2022. URL: https://doi.org/10.1007/S10817-021-09613-Z.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact