Home
Welcome
Welcome to my blog!
I am a computer engineer fascinated with math, theorem provers, type theory, and logic. I like to prove theorems in Agda, Lean, Idris, and KeY. I am doing my PhD at Chalmers University, improving the SoldiKeY theorem prover. After more than a year of studying cubical type theory and theorem provers, I decided to create this blog to share my ideas and thoughts.
Posts
- KeYther - January 7, 2026
- Using pattern-match in your favor - May 5, 2022
- How an Agda package in Nixpkgs should be - March 18, 2022
- Types for units of measure - December 18, 2021
- Concurrency language with small-step semantics - November 3, 2021
- Using small-step reduction in addition - October 30, 2021
- Using Containers in Agda - July 19, 2021
- Compressed lists in Cubical Agda - May 31, 2021
- Defining Natural Numbers using its associativity property in Agda - May 26, 2021
…or you can find more in the archives.