3 citations · 6 across the 3 of their papers we have counts for
Showing cs.LOShow all
3 papers · 1 filter
cs.LO2025
Subtyping in DHOL -- Extended preprint
Colin Rothgang, Florian Rabe
The recently introduced dependent typed higher-order logic (DHOL) offers an interesting compromise between expressiveness and automation support. It sacrifices the decidability of…
cs.LO2023★ 3 cited
Theorem Proving in Dependently-Typed Higher-Order Logic -- Extended Preprint
Colin Rothgang, Florian Rabe, Christoph Benzmüller
Higher-order logic HOL offers a very simple syntax and semantics for representing and reasoning about typed data structures. But its type system lacks advanced features where types…
cs.LO2017★ 3 cited
Alignment-based Translations Across Formal Systems Using Interface Theories
Dennis Müller, Colin Rothgang, Yufei Liu +1
Translating expressions between different logics and theorem provers is notoriously and often prohibitively difficult, due to the large differences between the logical foundations,…