Decomposition diversity with symmetric data and codata. - David Binder; Julian Jabs; Ingo Skupin; Klaus Ostermann (Proc. ACM Program. Lang., 2020)

Structural refinement types. - David Binder; Ingo Skupin; David Läwen; Klaus Ostermann (TyDe@ICFP, 2022)

Data-Codata Symmetry and its Interaction with Evaluation Order. - David Binder; Julian Jabs; Ingo Skupin; Klaus Ostermann (CoRR, 2022)

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

Getting into the Flow: Towards Better Type Error Messages for Constraint-Based Type Inference. - Ishan Bhanuka; Lionel Parreaux; David Binder; Jonathan Immanuel Brachthäuser (Proc. ACM Program. Lang., 2023)

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)

Grokking the Sequent Calculus (Functional Pearl). - David Binder; Marco Tzschentke; Marius Müller 003; Klaus Ostermann (Proc. ACM Program. Lang., 2024)

Programming with Symmetric Data and Codata Types. - David Binder (2024)

The Algebra of Patterns. - David Binder; Lean Ermantraut (ECOOP, 2025)

The Algebra of Patterns - Rocq Proofs (Artifact). - David Binder; Lean Ermantraut (Dagstuhl Artifacts Ser., 2025)

The Algebra of Patterns (Extended Version). - David Binder; Lean Ermantraut (CoRR, 2025)