personal photo of Nada Amin

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:2025
    Authors:
    Michael BallantyneRafaello SannaJason HemannWilliam E. ByrdNada Amin
    Description:

    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:2024
    Authors:
    Anastasiya Kravchuk-KirilyukGary FengJonas IskanderYizhou ZhangNada Amin
  • Extensible Metatheory Mechanization via Family Polymorphism

    Journal ArticlePublisher:Proc. ACM Program. Lang. (PLDI)Date:2023
    Authors:
    Ende JinNada AminYizhou Zhang
    Description:

    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:2022
    Authors:
    Yizhou ZhangNada Amin
  • A SQL to C compiler in 500 lines of code

    Journal ArticlePublisher:Journal of Functional ProgrammingDate:2019
    Authors:
    Tiark RompfNada Amin

Education

  • PhD

    from: 2011, until: 2016

    Field of study:Programming LanguagesSchool:EPFLLocation:Lausanne, Switzerland

    Description

    PhD Thesis: Dependent Object Types

  • BS & MEng

    from: 2001, until: 2008

    Field of study:Computer Science (Music Minor)School:MITLocation:Cambridge, MA, USA

    Description

    MEng 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: 2023

    Description:

    generating and verifying programs and proofs using LLMs, with a focus on Dafny and Python

  • collapsing towers for side-channel security

    date: 2022

    Organization: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 analysis

  • drug repurposing for precision medicine

    date: 2019

    Organization:led by the Hugh Kaul Precision Medicine Institute

  • multi-stage miniKanren

    date: 2017

    Description:

    multi-stage relational programming for fast synthesis from sketches

  • reflective towers of interpreters

    date: 2014

    Description:

    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: 2012

    Organization:EPFL

    Description:

    a type-theoretic foundation for languages like Scala

  • lightweight modular staging (LMS)

    date: 2011

    Organization:EPFL

    Description:

    led by Tiark Rompf, Scala/LMS exemplifies multi-stage programming, a principled approach to writing programs that write programs

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