Hi there! I'm Nat, a research engineer and PhD student in the Verified Software group at Imperial College London.
I've carried a passion for programming throughout my undergraduate studies and multiple industry positions, and now I'm taking my interests to the next level in striving for a PhD in PL research under Prof. Philippa Gardner, focusing on the user experience of program analysis tools.
After my final undergraduate project—where I developed a visual debugger for symbolic execution -based program analyses in the Gillian platform—I accepted the invitation to join the Verified Software group and continue this pursuit. This began with leveraging Gillian's parametric nature to explore language-agnostic symbolic execution debugging, before expanding the scope past Gillian to tool-agnostic debugging.
My work places me at an interstice between precise PL theory, subjective evaluation with diverse user groups, and raw software engineering; I find it incredibly rewarding.
In my free time, I love tinkering with my NixOS setup, experimenting with self-hosting, and exploring the artform of video games.
Core Skills
Symbolic verification
Since early 2022, I've been immersed in the world of symbolic verification via my work on Gillian. Creating a symbolic debugger required me to step deep into this concept, both in picking apart the process of execution and state matching, and formulating clear and concise ways of communicating execution traces to a user.Hoare & Separation Logic
My undergraduate studies involved specialist courses on Hoare Logic — including big- and small-step semantics — and Separation Logic for scalable program verification. My work frequently calls upon these principles, both in theoretical and practical contexts.OCaml proficiency
The history of formal methods is entwined with that of OCaml. I've grown a deep appreciation for the language while working in this field, arming me with a natural understanding of advanced techniques, including the monadic programming style, and abstracting via modules and functors.Polyglot
As a self-taught hobbyist, turned software engineer, turned research engineer, my experience ranges over many language paradigms — from C and Rust to Haskell and OCaml; from Java and Kotlin to Python and JavaScript. A prime example is how my symbolic debugger, introduced a second language (TypeScript) Gillian's codebase.Full stack
In my numerous engineering roles, I've worked on applications at all levels — frontend, backend, and databases — from development to deployment, and maintaining servers thereafter. I'm well-versed in collaboration via Git and GitHub, and I'm comfortable in various development environments, whether it be Windows, Linux, WSL or Docker.Achievements, Experience & Education
First class honours; transcript available upon request
6-month placement
3-month internship
Freelance contract
3-month internship
Contact me
I can most easily be contacted at:
- My personal e-mail, nat [at] karmios [dot] com .
- ...or failing that, my Imperial College email, n.karmios [at] ic [dot] ac [dot] uk .
You're more than welcome to reach out via LinkedIn, however I check it exceedingly rarely.
Special thanks to Philippa Gardner, Petar Maksimović and Sacha Ayoun for helping to form the foundation of my career in research.