Semantics for Dependently-Typed HOL
Rabe F (2026)
Publication Type: Conference contribution
Publication year: 2026
Journal
Publisher: Springer Science and Business Media Deutschland GmbH
Book Volume: 16689 LNCS
Pages Range: 143-160
Conference Proceedings Title: Lecture Notes in Computer Science
Event location: Lissabon
ISBN: 9783032325914
DOI: 10.1007/978-3-032-32592-1_9
Abstract
Both higher-order logic and dependent types are popular features for languages used for the formalization of complex domains. Recently DHOL was introduced as a language that provides the expressivity of dependent types while retaining the general feel of higher-order logic. Since then multiple extensions and theorem provers have been developed, and DHOL was adopted as the first TPTP standard for using dependent types in automated theorem provers. However, the literature lacks a model theoretical semantics for DHOL. The present paper fills in this gap, covering dependent types, rank-1 polymorphism, and functions with preconditions. It introduces both standard models and an appropriate generalization of Henkin-style models and proves soundness and completeness. Considerable care went into keeping the formulation as close to the usual definitions for HOL and elegant enough to serve as a reference point for language extensions and theorem provers for DHOL.
Authors with CRIS profile
How to cite
APA:
Rabe, F. (2026). Semantics for Dependently-Typed HOL. In Armin Biere, Carsten Lutz, Sara Negri (Eds.), Lecture Notes in Computer Science (pp. 143-160). Lissabon, PT: Springer Science and Business Media Deutschland GmbH.
MLA:
Rabe, Florian. "Semantics for Dependently-Typed HOL." Proceedings of the 13th International Joint Conference on Automated Reasoning, IJCAR 2026, Lissabon Ed. Armin Biere, Carsten Lutz, Sara Negri, Springer Science and Business Media Deutschland GmbH, 2026. 143-160.
BibTeX: Download