My research and technical interests revolve around various interrelated topics:
- Formal specification and verification, proof assistants
- Functional and logic programming, type systems
- Proof theory and sequent calculi, proofs and certificates
The grand unifying theme, and pragmatic motivation, is an ambition that I am convinced is both lofty and realistic: this is the need for trust and correctness — in theorems as in the entire pantheon of formalizable artifacts, with software as primus inter pares in today’s world — and a discipline that treats these as first-class abstractions.