A short list of selected software and mathematical formalisations I have worked on:

• Patch locale. Formalisation of a completely predicative construction of the patch locale (j.w.w. Martín Escardó) as part of TypeTopology.
• formal-topology-in-UF. Formalisation of some locale theory and formal topology in cubical type theory, originally developed to accompany my MSc thesis.
• Sierpiński frame in UF. An implementation of the Sierpiński frame using formal topology.
• Initial frame in TypeTopology. Formalisation of the initial frame in the TypeTopology library of
• sequents. A Standard ML implementation of Roy Dyckhoff's sequent calculus LJT.
• simplc. A toy compiler from a simple security-typed imperative language into a stack machine, formally verified to preserve the noninterference property of the high level language through compilation. Developed together with Alexander Fuhs as the final project for Andrei Sabelfeld's language-based security course at Chalmers.