Daniel Ranalter

Experiments with Choice in Dependently-Typed Higher-Order Logic

2024 · EPiC series in computing

Recently an extension to higher-order logic — called DHOL — was introduced, enrich- ing the language with dependent types, and creating a powerful extensional type theory. In this paper we propose two ways how choice …