"Dependently typed higher-order logic" - New article in ACM journal

The article “Dependently-Typed Higher-Order Logic” co-authored by Prof. Christoph Benzmüller has just appeared in the ACM Transactions on Computational Logic: https://dl.acm.org/doi/10.1145/3771725. The paper evolved out of the maths masters thesisof Colin Rothgang at FU Berlin (now at Imdea Software Institute, Spain and Universidad Politécnica de Madrid, Spain), which was supervised by Benzmüller and Florian Rabe (FAU Erlangen).