Introduction and elimination, left and right. - Klaus Ostermann; David Binder; Ingo Skupin; Tim Süberkrüb; Paul Downen (Proc. ACM Program. Lang., 2022)

Deriving Dependently-Typed OOP from First Principles - Extended Version with Additional Appendices. - David Binder; Ingo Skupin; Tim Süberkrüb; Klaus Ostermann (CoRR, 2024)

Deriving Dependently-Typed OOP from First Principles. - David Binder; Ingo Skupin; Tim Süberkrüb; Klaus Ostermann (Proc. ACM Program. Lang., 2024)