Nada Amin
Tagline:assistant professor (PL+AI) at Harvard SEAS
Cambridge, MA, USA
About Me
I like to program and metaprogram, i.e., explore new ways of programming.
I combine programming languages (PL) and artificial intelligence (AI), including large language models (LLMs), to create intelligent systems that are correct by construction. My current application domains include program and proof synthesis, and precision medicine.
Research Interests
- meta-theory of modular, extensible systems for programming and proving
- meta-programming around multi-stage programming and reflection
- meta-reasoning in relational & probabilistic programming
- neurosymbolic AI/PL like relaxing machines from symbolic to differentiable
- verified program and proof synthesis mixing symbolic reasoning and LLMs
- verified discovery systems for programming and mathematics
- precision medicine to explore collaborative problem-solving agents
- softening verification to validation by learning strategies in the easier hard setting
Publications
Multi-stage Relational Programming
Journal ArticlePublisher:Proc. ACM Program. Lang.Date:2025Authors:Michael BallantyneRafaello SannaJason HemannWilliam E. ByrdNada AminDescription:We transport multi-stage programming from functional to relational programming, with novel constructs to give programmers control over staging and non-determinism. We stage interpreters written as relations, in which the programs under interpretation can contain holes representing unknown expressions or values. By compiling the known parts without interpretive overhead and deferring interpretation to run time only for the unknown parts, we compound the benefits of staging (e.g., turning interpreters into compilers) and relational interpretation (e.g., turning functions into relations and synthesizing from sketches). We extend miniKanren with staging constructs and apply the resulting multi-stage language to relational interpreters for subsets of Racket and miniKanren as well as a relational recognizer for context-free grammars. We demonstrate significant performance gains across multiple synthesis problems, systematically comparing unstaged and staged computation, as well as indicatively comparing with an existing hand-tuned relational interpreter.
Persimmon: Nested Family Polymorphism with Extensible Variant Types
Journal ArticlePublisher:Proc. ACM Program. Lang. (OOPSLA)Date:2024Authors:Anastasiya Kravchuk-KirilyukGary FengJonas IskanderYizhou ZhangNada AminExtensible Metatheory Mechanization via Family Polymorphism
Journal ArticlePublisher:Proc. ACM Program. Lang. (PLDI)Date:2023Authors:Ende JinNada AminYizhou ZhangDescription:Distinguished Paper Award
Reasoning about “Reasoning about Reasoning”: Semantics and Contextual Equivalence for Probabilistic Programs with Nested Queries and Recursion
Journal ArticlePublisher:Proc. ACM Program. Lang. (POPL)Date:2022Authors:Yizhou ZhangNada Amin
Education
PhD
from: 2011, until: 2016Field of study:Programming LanguagesSchool:EPFLLocation:Lausanne, Switzerland
DescriptionPhD Thesis: Dependent Object Types
BS & MEng
from: 2001, until: 2008Field of study:Computer Science (Music Minor)School:MITLocation:Cambridge, MA, USA
DescriptionMEng Thesis: Computer-Aided Design for Multilayer Microfluidic Chips
Teaching
CS152 (every Spring)
From: 2020, Until: present
Organization:HarvardField:Programming Languages
Description:undergraduate class, introducing the theory, design, and implementation of programming languages, including formal semantics, type systems, and lambda calculus
CS252R (every Fall)
From: 2019, Until: present
Organization:HarvardField:Advanced Topics in Programming Languages
Description:graduate seminar where the topic changes each year. Past editions: PL+HCI (2019), PL+AI (2020), PL design (2021), advanced semantics (2022), program synthesis (2023), PL theory & implementation (2024)
Metaprogramming
From: 2018, Until: 2019
Organization:University of CambridgeField:Programming Languages
Description:principled approaches to metaprogramming: writing programs that manipulate programs, including evaluators, reflection, multi-stage programming, DSLs, meta-linguistic abstractions, and synthesis
Research Projects
verified program synthesis
date: 2023Description:generating and verifying programs and proofs using LLMs, with a focus on Dafny and Python
collapsing towers for side-channel security
date: 2022Organization:Harvard & MIT
Description:specializing a program wrt a hardware processor as a staged interpreter
making micro-architectural details such as timing explicit and first-order for off-the-shelf analysisdrug repurposing for precision medicine
date: 2019Organization:led by the Hugh Kaul Precision Medicine Institute
multi-stage miniKanren
date: 2017Description:multi-stage relational programming for fast synthesis from sketches
reflective towers of interpreters
date: 2014Description:a reflective meta-level architecture where each level has a meta level ad infinitum with historical artifacts 3-LISP, Brown, Blond, Black in the 80s & 90s, and our Pink & Purple in POPL’18
I’ve been fascinated by principled approaches to reflection, combining multiple paradigms (e.g., not just functional but also relational), and supporting effective reasoning and even verification. After all, proof by reflection has a venerable tradition starting with FOL’78.
dependent object types (DOT)
date: 2012Organization:EPFL
Description:a type-theoretic foundation for languages like Scala
lightweight modular staging (LMS)
date: 2011Organization:EPFL
Description:led by Tiark Rompf, Scala/LMS exemplifies multi-stage programming, a principled approach to writing programs that write programs
GitHub Topics
topics(with count of selected projects): scheme17 paper-implementations15 ai14 reflection11 llm10 generative-programming8 scala8 towers8 clojure7 logic-programming6 minikanren6 binders5 coq5 dafny5 synthesis5 verification5 collapsing-towers4 common-lisp4 metaprogramming4 multi-stage-programming4 reasoning4 c3 constraints3 meta-theory3 monte-carlo-tree-search3 music3 oop3 python3 racket3 data-science2 logic2 machine-learning2 meta2 ncats-translator2 prolog2 smt2 truth-maintenance2 tutorial2 a-star-search1 abstract-interpretation1 chatgpt1 communication-bootstrapping1 compiler1 compiler-construction1 composition1 coq-formalization1 differentiable-programming1 discovery-system1 docker1 expert-system1 frama-c1 github1 harmony1 interactive1 interpreters1 java1 jax1 jit1 lean1 lisp1 mcp1 meta-reasoning1 metabolic-network1 neuro-symbolic1 overtone1 plt-redex1 program-transformations1 proofsketcher1 rocq1 theorem-prover1 twelf1 unsound1 workshop1 x861
Bio
I am an assistant professor of computer science at Harvard SEAS. Previously, I was a University Lecturer in Programming Languages at the University of Cambridge; a member of the team behind the Scala programming language at the Ecole Polytechnique Federale de Lausanne (EPFL), where I pursued my PhD; and a software engineer at Google, on the compiler infrastructure supporting Gmail and other Google Apps. I hold bachelor of science and master of engineering degrees from the Massachusetts Institute of Technology (MIT).