Home GOTO Experts Nada Amin

Nada Amin

Assistant Professor of Computer Science at Harvard SEAS

Nada Amin is an Assistant Professor of Computer Science at Harvard SEAS. Prior to this, she was a University Lecturer in Programming Languages at the University of Cambridge and part of the team behind the Scala programming language at École Polytechnique Fédérale de Lausanne (EPFL), where she completed her PhD. She also worked as a software engineer at Google, contributing to the compiler infrastructure behind Gmail and other Google Apps. Nada holds a Bachelor of Science and a Master of Engineering from the Massachusetts Institute of Technology (MIT).

Upcoming conference sessions featuring Nada Amin

Metaprogramming, Synthesis, and Verification

With live examples Nada will demonstrate:

  • Dafny and verification-aware programming, including proof by induction to verify properties of programs (for example, that an optimizer preserves semantics).
  • Multi-stage programming, a principled approach to writing programs that write programs, and its incarnation in multi-stage relational programming for faster synthesis of programs with holes—with the theoretical insight that a staged interpreter is a compiler, and a staged relational interpreter for a functional language can turn functions into relations running backwards for synthesis.
  • Monte Carlo Tree Search, specifically the VerMCTS variant, and when this exploration-exploitation sweet spot is a good match for synthesis problems.

The ideas will be demonstrated with live examples and open-source artifacts spanning verified programming, relational programming, and LLM-guided synthesis, including Dafny Sketcher (https://github.com/namin/dafny-sketcher), multi-stage miniKanren (https://github.com/namin/staged-miniKanren), VerMCTS (https://github.com/namin/llm-verified-with-monte-carlo-tree-search), and Holey (https://github.com/namin/holey).

Friday Dec 12 @ 13:15 @ YOW! Sydney 2025

Get conference pass

Metaprogramming, Synthesis, and Verification

With live examples Nada will demonstrate:

  • Dafny and verification-aware programming, including proof by induction to verify properties of programs (for example, that an optimizer preserves semantics).
  • Multi-stage programming, a principled approach to writing programs that write programs, and its incarnation in multi-stage relational programming for faster synthesis of programs with holes—with the theoretical insight that a staged interpreter is a compiler, and a staged relational interpreter for a functional language can turn functions into relations running backwards for synthesis.
  • Monte Carlo Tree Search, specifically the VerMCTS variant, and when this exploration-exploitation sweet spot is a good match for synthesis problems.

The ideas will be demonstrated with live examples and open-source artifacts spanning verified programming, relational programming, and LLM-guided synthesis, including Dafny Sketcher (https://github.com/namin/dafny-sketcher), multi-stage miniKanren (https://github.com/namin/staged-miniKanren), VerMCTS (https://github.com/namin/llm-verified-with-monte-carlo-tree-search), and Holey (https://github.com/namin/holey).

Tuesday Dec 9 @ 13:15 @ YOW! Brisbane 2025

Get conference pass

Metaprogramming, Synthesis, and Verification

With live examples I will demonstrate:

  • Dafny and verification-aware programming, including proof by induction to verify properties of programs (for example, that an optimizer preserves semantics).
  • Multi-stage programming, a principled approach to writing programs that write programs, and its incarnation in multi-stage relational programming for faster synthesis of programs with holes—with the theoretical insight that a staged interpreter is a compiler, and a staged relational interpreter for a functional language can turn functions into relations running backwards for synthesis.
  • Monte Carlo Tree Search, specifically the VerMCTS variant, and when this exploration-exploitation sweet spot is a good match for synthesis problems.

The ideas will be demonstrated with live examples and open-source artifacts spanning verified programming, relational programming, and LLM-guided synthesis, including Dafny Sketcher (https://github.com/namin/dafny-sketcher), multi-stage miniKanren (https://github.com/namin/staged-miniKanren), VerMCTS (https://github.com/namin/llm-verified-with-monte-carlo-tree-search), and Holey (https://github.com/namin/holey).

Friday Dec 5 @ 13:15 @ YOW! Melbourne 2025

Get conference pass

Browse all experts

Here