Subtyping in DHOL -- Extended preprint

TL;DR

This paper extends the expressive dependent typed higher-order logic (DHOL) with refinement and quotient types by leveraging its translation to HOL, enabling advanced type features while maintaining soundness and completeness.

Contribution

It introduces a novel extension of DHOL with refinement and quotient types as subtypes, simplifying their integration and preserving logical properties.

Findings

Successfully added refinement and quotient types to DHOL

Maintained soundness and completeness in the extended logic

Provided syntax, semantics, and translation to HOL

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.