Liquid Amortization: Proving Amortized Complexity with LiquidHaskell (Functional Pearl). - Jan van Brügge (Haskell, 2024)

Barendregt Convenes with Knaster and Tarski: Strong Rule Induction for Syntax with Bindings. - Jan van Brügge; James McKinna; Andrei Popescu 001; Dmitriy Traytel (Proc. ACM Program. Lang., 2025)