Nada Amin
Tagline:assistant professor (PL+AI) at Harvard SEAS
Cambridge, MA, USA
About Me
I like to hack and meta-hack, 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
- precision medicine to explore collaborative problem-solving agents
Publications
Persimmon: Nested Family Polymorphism with Extensible Variant Types
Journal ArticlePublisher:Proc. ACM Program. Lang. (OOPSLA)Date:2024Authors:Anastasiya Kravchuk-KirilyukGary FengJonas IskanderYizhou ZhangNada AminThe Dolorem Pattern: Growing a Language through Compile-Time Function Execution
Conference PaperPublisher:37th European Conference on Object-Oriented Programming, ECOOP, July 17-21, Seattle, Washington, USADate:2023Authors:Simon HennigerNada 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 ScienceSchool: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: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
(with count of selected projects): scheme17 paper-implementations15 reflection11 ai10 clojure7 scala7 towers7 generative-programming6 logic-programming6 minikanren6 binders5 llm5 common-lisp4 coq4 reasoning4 c3 collapsing-towers3 dafny3 meta-theory3 metaprogramming3 multi-stage-programming3 music3 oop3 racket3 synthesis3 constraints2 logic2 meta2 monte-carlo-tree-search2 ncats-translator2 prolog2 python2 truth-maintenance2 tutorial2 verification2
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 her 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).