Jesper Cockx

Optimising First-Class Pattern Matching

2022

Pattern matching is a high-level notation for programs to analyse the shape of data, and can be optimised to efficient low-level instructions. The Stratego language uses first-class pattern matching, a powerful form of pattern matching …

Enhancing Interactive Theorem Prover Error Messages with Hints

2026 · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics)

Interactive theorem provers (ITPs) are promising tools for ensuring program correctness, but users often complain about their poor usability and steep learning curve. A common complaint, especially among new users, are confusing error messages that …