Nachi Valliappan

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.

Current

I am a Royal Society Newton International Fellow in the Laboratory for Foundations of Computer Science at the University of Edinburgh.

Ongoing projects:

• Compositional Normalization with Modal Types (page, proposal)

Dormant projects:

• Fitch-Style Modal Lambda Calculi: Meta-theory and Applications (page)
  with Fabian Ruch and Carlos Tomé Cortiñas.

• Extensible Normalization and Partial Evaluation (page)
  with Sam Lindley and Ohad Kammar.

Publications

• Kripke-Style Semantics of Strong Functors (pdf)
  Draft. 2025.

• 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.

• Towards Adding Variety to Simplicity (pdf, doi)
  ISoLA 2018.

• Typing the Wild in Erlang (pdf, doi)
  Erlang 2018.

• Typing the Untypeable in Erlang (uri)
  Chalmers MSc thesis. 2018.

Abstracts, etc.

• 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.

Teaching

• 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.

Supervision

• 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.

Talks

• modal (propositions as types) (video, slides)
  TUPLES, Feb ‘25

• 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.

• Normalization for Fitch-Style Modal Calculi
  • Gothenburg University Logic Seminar, Sep ‘21 (slides, abstract).
  • Scottish Programming Languages Seminar, Jul ‘22 (slides, abstract).
  • International Conference on Functional Programming, Sep ‘22 (video, slides, abstract).
  • Programming Languages Seminar at University of Bristol, Oct ‘22.

• 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.

• Be My Guest (slides, abstract)
  Licentiate Seminar, Dec ‘20.

• 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.

• Typing the Wild in Erlang (video, slides, abstract)
  Erlang Workshop, Sep ‘18.

Past gigs

• Masters and PhD at Chalmers University of Technology, Sweden
• Summer student at CERN, Switzerland
• Freelance backend developer
• Backend engineer at Shieldsquare and Acrodelon
• Bachelors at National Institute of Technology Calicut, India

Contact

nachivpn[at]gmail.com