3 citations · 6 across the 3 of their papers we have counts for
4 papers
Lava: Foundations for Liquid Haskell via Translation to Rocq
Colin Rothgang, Loïc Peyrot, Yannick Forster +2
Liquid Haskell is an extension of the Glasgow Haskell compiler (GHC) that adds support for refinement types: types restricted by logical predicates. Specifications are automaticall…
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…
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…
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,…