1. The Modular Imperative: Rethinking LLMs for Maintainable Software (Proceedings of the 1st ACM SIGPLAN International Workshop on Language Models and Programming Languages (LMPL’25), 2025) by Anastasiya Kravchuk-Kirilyuk, Fernanda Graciolli, and Nada Amin
  2. Semantics of the memo Probabilistic Programming Language (POPL Workshop on Languages for Inference (LAFI), 2025) by Kartik Chandra, Nada Amin, and Yizhou Zhang
  3. ⭐Multi-stage Relational Programming (PLDI 2025) by Michael Ballantyne, Rafaello Sanna, Jason Hemann, William Byrd, and Nada Amin (Code: https://github.com/namin/staged-miniKanren)
  4. Guided Proof Search Using Large Language Models and Lemma Extraction in Coq (ICLR Workshop: VerifAI: AI Verification in the Wild, 2025) by Tarun Prasad and Nada Amin (Code: https://github.com/mtarunpr/coq-prover)
  5. Collapsing towers for side-channel security (Short Paper) (PEPM, 2025) by Cameron Wong, Muhammad Abdullah, Yuheng Yan, Mengjia Yan, Adam Chlipala, and Nada Amin (Code: https://github.com/namin/lms-koika)
  6. Multi-objective generative AI for designing novel brain-targeting small molecules (ICLR Workshop on Generative and Experimental Perspectives for Biomolecular Design, 2024) by Ayush Noori, Iñaki Arango, William Byrd, and Nada Amin (Code: https://github.com/ayushnoori/molecule-synthesis)
  7. dafny-annotator: AI-Assisted Verification of Dafny Programs (2024) by Gabriel Poesia, Chloe Loughridge, and Nada Amin (Code: https://github.com/metareflection/dafny-annotator)
  8. DafnyBench: A Benchmark for Formal Software Verification (2024) by Chloe Loughridge, Qinyi Sun, Seth Ahrenbach, Federico Cassano, Chuyue Sun, Ying Sheng, Anish Mudide, Md Misu, Nada Amin, and Max Tegmark (Code: https://github.com/sun-wendy/DafnyBench)
  9. VerMCTS: Synthesizing Multi-Step Programs using a Verifier, a Large Language Model, and Tree Search (2024) by David Brandfonbrener, Simon Henniger, Sibi Raja, Tarun Prasad, Chloe Loughridge, Federico Cassano, Sabrina Hu, Jianang Yang, William Byrd, Robert Zinkov, and Nada Amin (Code: https://github.com/namin/llm-verified-with-monte-carlo-tree-search) Outstanding Paper Award at MATH-AI co-located with NeurIPS
  10. ⭐Persimmon: Nested Family Polymorphism with Extensible Variant Types (OOPSLA 2024) by Anastasiya Kravchuk-Kirilyuk, Gary Feng, Jonas Iskander, Yizhou Zhang, and Nada Amin (Code: https://github.com/akravc/persimmon)
  11. Oxidize: A Step-Debugger for Static Semantics (IWACO, 2023) by Peter Chon, Dimi Racordon, and Nada Amin
  12. ⭐The Dolorem Pattern: Growing a Language through Compile-Time Function Execution (ECOOP 2023) by Simon Henniger and Nada Amin (Code: https://github.com/shenniger/dolorem)
  13. LURK: Lambda, the Ultimate Recursive Knowledge (Experience Report) (ICFP 2023) by Nada Amin, John Burnham, François Garillot, Rosario Gennaro, Chhi’m`ed K"unzang, Daniel Rogozin, and Cameron Wong
  14. ⭐Extensible Metatheory Mechanization via Family Polymorphism (PLDI 2023) by Ende Jin, Nada Amin, and Yizhou Zhang (Code: https://github.com/DKXXXL/FPOP) Distinguished Paper Award
  15. ⭐The precision medicine process for treating rare disease using the artificial intelligence tool mediKanren (Frontiers in artificial intelligence, 2022) by Aleksandra Foksinska, Camerron Crowder, Andrew Crouse, Jeff Henrikson, William Byrd, Gregory Rosenblatt, Michael Patton, Kaiwen He, Thi Tran-Nguyen, Marissa Zheng, Stephen Ramsey, Nada Amin, John Osborne, UAB Precision Medicine Institute, and Matthew Might
  16. ⭐Reasoning about “Reasoning about Reasoning”: Semantics and Contextual Equivalence for Probabilistic Programs with Nested Queries and Recursion (POPL 2022) by Yizhou Zhang and Nada Amin (Code: https://github.com/yizhouzhang/rrr-popl2022-coq)
  17. A Pearl Pearl: how to teach an old AI new tricks (PROBPROG (poster), 2021) by Nada Amin, William Byrd, Joseph Cottam, Marc-Antoine Parent, and Jeremy Zucker (Code: https://github.com/namin/biohacker)
  18. ⭐Technical Perspective: Programming Microfluidics to Execute Biological Protocols (Commun. ACM, 2021) by Nada Amin
  19. Reflective Towers of Interpreters, SIGPLAN PL Perspectives (2021) by Nada Amin (More info: https://blog.sigplan.org/2021/08/12/reflective-towers-of-interpreters)
  20. Family Polymorphism for Proof Extensibility (TYPES (Extended Abstract), 2021) by Anastasiya Kravchuk-Kirilyuk, Yizhou Zhang, and Nada Amin (More info: https://types21.liacs.nl/download/family-polymorphism-for-proof-extensibility)
  21. Prototypes: Object-Orientation, Functionally (Scheme and Functional Programming Workshop, 2021) by François-René Rideau, Alex Knauth, and Nada Amin (Code: https://github.com/metareflection/poof)
  22. Prolog-Style Meta-Programming miniKanren (miniKanren and Relational Programming Workshop, 2021) by Nada Amin, William Byrd, and Tiark Rompf (Code: https://github.com/namin/metamk)
  23. mediKanren: a System for Biomedical Reasoning (miniKanren and Relational Programming Workshop, 2020) by William Byrd, Gregory Rosenblatt, Michael Patton, Thi Tran-Nguyen, Marissa Zheng, Apoorv Jain, Michael Ballantyne, Katherine Zhang, Mei-Jan Chen, Jordan Whitlock, Mary Crumbley, Jillian Tinglin, Kaiwen He, Yizhou Zhang, Jeremy Zucker, Joseph Cottam, Nada Amin, John Osborne, Andrew Crouse, and Matthew Might (Code: https://github.com/webyrd/mediKanren)
  24. ⭐A SQL to C compiler in 500 lines of code (Journal of Functional Programming, 2019) by Tiark Rompf and Nada Amin (More info: https://scala-lms.github.io/tutorials/query.html)
  25. Lightweight Functional Logic Meta-Programming (Programming Languages and Systems (APLAS), 2019) by Nada Amin, William Byrd, and Tiark Rompf (Code: https://github.com/namin/scalogno)
  26. Representing Music with Prefix Trees (Proceedings of the 7th ACM SIGPLAN International Workshop on Functional Art, Music, Modeling, and Design, 2019) by Yan Han, Nada Amin, and Neel Krishnaswami
  27. ⭐Collapsing Towers of Interpreters (POPL 2018) by Nada Amin and Tiark Rompf (Code: http://popl18.namin.net)
  28. ⭐Versatile Event Correlation with Algebraic Effects (ICFP 2018) by Oliver Bračevac, Nada Amin, Guido Salvaneschi, Sebastian Erdweg, Patrick Eugster, and Mira Mezini
  29. ⭐LMS-Verify: Abstraction without Regret for Verified Systems Programming (POPL 2017) by Nada Amin and Tiark Rompf (Code: https://github.com/namin/lms-verify)
  30. ⭐Type Soundness Proofs with Definitional Interpreters (POPL 2017) by Nada Amin and Tiark Rompf (Code: http://popl17.namin.net)
  31. ⭐Type Soundness for Dependent Object Types (DOT) (OOPSLA 2016) by Tiark Rompf and Nada Amin (Code: http://oopsla16.namin.net)
  32. ⭐Java and Scala’s Type Systems Are Unsound: The Existential Crisis of Null Pointers (OOPSLA 2016) by Nada Amin and Ross Tate (More info: https://io.livecode.ch/learn/namin/unsound) Distinguished Artifact Award
  33. ⭐The Essence of Dependent Object Types (A List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday, 2016) by Nada Amin, Samuel Gr"utter, Martin Odersky, Tiark Rompf, and Sandro Stucki (Code: http://wadlerfest.namin.net)
  34. ⭐Functional Pearl: A SQL to C Compiler in 500 Lines of Code (ICFP 2015) by Tiark Rompf and Nada Amin (More info: https://scala-lms.github.io/tutorials/query.html)
  35. ⭐Foundations of Path-Dependent Types (Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages \ Applications, 2014) by Nada Amin, Tiark Rompf, and Martin Odersky (Code: http://oopsla14.namin.net)
  36. Mind the gap: Artifacts vs insights in PL theory. (Off-the-Beaten Track (OBT), 2014) by Nada Amin and Tiark Rompf (More info: https://popl-obt-2014.cs.brown.edu/papers/gap.pdf)
  37. Computing with an SMT Solver (Tests and Proofs, 2014) by Nada Amin, K. Leino, and Tiark Rompf
  38. ⭐Optimizing Data Structures in High-Level Programs: New Directions for Extensible Compilers Based on Staging (POPL 2013) by Tiark Rompf, Arvind Sujeeth, Nada Amin, Kevin Brown, Vojin Jovanovic, HyoukJoong Lee, Manohar Jonnalagedda, Kunle Olukotun, and Martin Odersky
  39. What Are the Odds? Probabilistic Programming in Scala (Proceedings of the 4th Workshop on Scala, 2013) by Sandro Stucki, Nada Amin, Manohar Jonnalagedda, and Tiark Rompf
  40. A Flow-Insensitive, Modular Effect System for Purity (Proceedings of the 15th Workshop on Formal Techniques for Java-like Programs, 2013) by Lukas Rytz, Nada Amin, and Martin Odersky
  41. Dafny for Metatheory of Programming Languages (2012) by Nada Amin (Code: https://github.com/namin/dafny-sandbox)
  42. Dependent Object Types (19th International Workshop on Foundations of Object-Oriented Languages, Tucson, Arizona, USA, 2012) by Nada Amin, Adriaan Moors, and Martin Odersky (Code: https://github.com/namin/dot)
  43. ⭐Scala-Virtualized: Linguistic Reuse for Deep Embeddings (Higher Order Symbol. Comput., 2012) by Tiark Rompf, Nada Amin, Adriaan Moors, Philipp Haller, and Martin Odersky
  44. ⭐JavaScript as an Embedded DSL (ECOOP 2012) by Grzegorz Kossakowski, Nada Amin, Tiark Rompf, and Martin Odersky (Code: https://github.com/js-scala)
  45. Computer-aided design for microfluidic chips based on multilayer soft lithography (IEEE International Conference on Computer Design, 2009) by Nada Amin, William Thies, and Saman Amarasinghe (More info: http://groups.csail.mit.edu/cag/micado)
  46. ⭐Cytoscape: a software environment for integrated models of biomolecular interaction networks (Genome Res., 2003) by Paul Shannon, Andrew Markiel, Owen Ozier, Nitin Baliga, Jonathan Wang, Daniel Ramage, Nada Amin, Benno Schwikowski, and Trey Ideker (More info: https://cytoscape.org)
  47. ⭐Global architecture of genetic interactions on the protein network (Nat. Biotechnol., 2003) by Owen Ozier, Nada Amin, and Trey Ideker