I study the design and implementation of programming languages using a combination of tools from formal logic and mathematical (or “denotational”) semantics. My specific research interests include type systems, language-based security and functional programming. I care about teaching and take active interest in the history and philosophy of science.
I am a Royal Society Newton International Fellow in the Laboratory for Foundations of Computer Science at the University of Edinburgh.
Ongoing projects:
Dormant projects:
Fitch-Style Modal Lambda Calculi: Meta-theory and Applications (homepage)
with Fabian Ruch and Carlos Tomé Cortiñas.
Extensible Normalization and Partial Evaluation (homepage)
with Sam Lindley and Ohad Kammar.
Kripke-Style Semantics for Strong Functors (pdf)
Draft. 2024.
Modular Normalization with Types (pdf)
Chalmers PhD thesis. 2023.
Normalization for Fitch-Style Modal Calculi (pdf, doi, arxiv)
ICFP 2022. Distinguished paper.
Practical Normalization by Evaluation for EDSLs (pdf, doi)
Haskell 2021.
Towards Secure IoT Programming in Haskell (pdf, doi)
Haskell 2020.
Simple Noninterference by Normalization (pdf, doi)
PLAS 2019.
Exponential Elimination for Bicartesian Closed Categorical Combinators (pdf, doi)
PPDP 2019.
Fitch-Style Applicative Functors (Extended Abstract) (pdf)
Draft. 2023.
Normalization by Evaluation with Free Extensions (Extended Abstract) (pdf)
TyDe 2022.
Normalization for Fitch-Style Modal Calculi (Extended Abstract) (pdf)
TYPES 2021.
Logic in Computer Science (DAT060/DIT202)
TA at Chalmers/GU, 2019-2022.
Testing, Debugging and Verification (TDA567/DIT083)
TA at Chalmers/GU, 2019-2022.
Finite Automata and Formal Languages (TMV028/DIT322)
TA at Chalmers/GU, 2020-2023.
Data Structures (DAT037)
TA at Chalmers, 2018.
A Parametric Fitch-Style Modal Lambda Calculus (proposal, code, thesis)
Master thesis by Axel Forsman, Jan-Jun ‘23.
Towards Normalization by Evaluation for Erlang (original proposal, thesis)
Master thesis by Carl Agrell and Haohan Yang, Jan-Jun ‘23.
Modular Normalization with Types (slides)
PhD Defence, May ‘23.
Normalization by Evaluation with Free Extensions (video, slides, abstract)
Workshop on Type-Driven Development, Sep ‘22.
Retrofitting Impure Languages with Static Information-Flow Control (slides, abstract)
Chalmers Security Seminar, Dec ‘21.
Practical Normalization by Evaluation for EDSLs (video, slides, abstract)
Haskell Symposium, Aug ‘21.
Modal λ-Calculi: Fitch vs. Dual-Context Style (representing Fitch-Style) (video, abstract)
Initial Types Club, Mar ‘21.
Boxes and Locks (slides)
Proglog Seminar, Dec ‘20.
Towards Secure IoT Programming in Haskell (video, slides, abstract)
Haskell Symposium, Aug ‘20.
Categorical Combinators (abstract)
Initial Types Club, Apr ‘20.
From syntax to semantics and back: Demystifying NbE (abstract)
Initial Types Club, Dec ‘19.
nachivpn[at]gmail.com