Experiments with Choice in Dependently-Typed Higher-Order Logic. - Daniel Ranalter; Chad E. Brown; Cezary Kaliszyk (LPAR, 2024)

The Dependently Typed Higher-Order Form for the TPTP World. - Daniel Ranalter; Cezary Kaliszyk; Florian Rabe 001; Geoff Sutcliffe (CoRR, 2025)