I'm a PhD student in "A Small Formal Methods Group" at NTU Singapore, supervised by Yong Kiam Tan. Before that I studied at ETH Zurich, where I completed my Bachelor's and Master's degrees in Computer Science. During my Master's, I had the opportunity to do an internship with Magnus Myreen, through whom I've met Yong Kiam Tan, leading to our work on improving Dafny's trustworthiness using the HOL4 theorem prover.
My current research focuses on improving Candle, a fully verified clone of HOL Light that runs on top of CakeML, a verified implementation of Standard ML. My aim is for Candle to be able to run existing proof developments efficiently, including proofs by D. J. Bernstein, the s2n-bignum proofs, and the HOL Light parts of Flyspeck.
Beyond this, I'm interested in applying foundational formal methods to other areas, such as automated reasoning or quantum computing. I would also like to explore automated reasoning and artificial intelligence more generally. Please reach out if you'd like to collaborate (or just chat).
Daniel Nezamabadi, Magnus Myreen, Yong Kiam Tan
CPP 2026 (Paper, Talk, Slides, Code, Poster)
Formalization of a verified verification condition generator and verified compiler for an imperative subset of Dafny using HOL4.
Daniel Nezamabadi, Magnus Myreen
Dafny 2025 (Paper, Talk, Slides)
Implementation of a compiler for a subset of Dafny by targeting CakeML using HOL4.
Supervised by Isaac van Bakel and Ralf Jung
Research in Computer Science @ ETH Zurich (2025) (Slides, Code)
Verification of add and remove described in
A Lazy Concurrent
List-Based Set Algorithm
using Iris
and Rocq.
Supervised by João C. Pereira and Peter Müller
Practical Work @ ETH Zurich (2024) (Report, Code)
Implementation of a library of definitions and lemmas used in specifications and proofs for Gobra.