PhD student at Chalmers University advised by Alejandro Russo (expected to graduate in 2023). I study programming languages, and my research interests include type systems, functional programming, and language-based security. I take active interest in teaching and historical aspects of my research.
Extensible Normalization and Partial Evaluation (project)
with Sam Lindley and Ohad Kammar.
Modal Lambda Calculi: Meta-theory and Applications (project)
with Fabian Ruch and Carlos Tomé Cortiñas.
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.
Partial Evaluator for Erlang (proposal)
Master thesis, 2023-now.
A Parametric Fitch-Style Modal Lambda Calculus (proposal)
Master thesis, 2023-now.
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