• 2026-05-03

  Total parser combinators with graded monads
• 2021-06-02

  Using dependent types to write proofs in Haskell
• 2019-09-07

  Run-length encoding verified in Agda
• 2019-05-19

  An Agda eDSL for well-typed Hilbert style proofs