Subtyping in Dependently-Typed Higher-Order Logic
Rothgang C, Rabe F (2026)
Publication Type: Conference contribution
Publication year: 2026
Journal
Publisher: Springer Science and Business Media Deutschland GmbH
Book Volume: 15979 LNAI
Pages Range: 98-114
Conference Proceedings Title: Lecture Notes in Computer Science
Event location: Reykjavik, ISL
ISBN: 9783032041661
DOI: 10.1007/978-3-032-04167-8_6
Abstract
The recently introduced dependent typed higher-order logic (DHOL) offers an interesting compromise between expressiveness and automation support. It sacrifices the decidability of its type system in order to significantly extend its expressiveness over standard HOL. Yet it retains strong automated theorem proving support via a sound and complete translation to HOL. We leverage this design to extend DHOL with refinement and quotient types. Both of these are commonly requested by practitioners but rarely provided by automated theorem provers. This is because they inherently require undecidable typing and thus are very difficult to retrofit to decidable type systems. But with DHOL already doing the heavy lifting, adding them is not only possible but elegant and simple. Concretely, we add refinement and quotient types as special cases of subtyping. This turns the associated canonical inclusion resp. projection maps into identity maps and thus avoids costly changes in representation. We present the syntax, semantics, and translation to HOL for the extended language, including the proofs of soundness and completeness.
Authors with CRIS profile
Involved external institutions
Spain (ES)How to cite
APA:
Rothgang, C., & Rabe, F. (2026). Subtyping in Dependently-Typed Higher-Order Logic. In René Thiemann, Christoph Weidenbach (Eds.), Lecture Notes in Computer Science (pp. 98-114). Reykjavik, ISL: Springer Science and Business Media Deutschland GmbH.
MLA:
Rothgang, Colin, and Florian Rabe. "Subtyping in Dependently-Typed Higher-Order Logic." Proceedings of the 15th International Symposium on Frontiers of Combining Systems, FroCoS 2025, Reykjavik, ISL Ed. René Thiemann, Christoph Weidenbach, Springer Science and Business Media Deutschland GmbH, 2026. 98-114.
BibTeX: Download