1. ⭐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)
  2. 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)
  3. 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)
  4. 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)
  5. dafny-annotator: AI-Assisted Verification of Dafny Programs (2024) by Gabriel Poesia, Chloe Loughridge, and Nada Amin (Code: https://github.com/metareflection/dafny-annotator)
  6. 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)
  7. 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
  8. ⭐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)
  9. ⭐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)
  10. 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
  11. ⭐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
  12. ⭐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
  13. ⭐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)
  14. 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)
  15. ⭐Technical Perspective: Programming Microfluidics to Execute Biological Protocols (Commun. ACM, 2021) by Nada Amin
  16. Reflective Towers of Interpreters, SIGPLAN PL Perspectives (2021) by Nada Amin (More info: https://blog.sigplan.org/2021/08/12/reflective-towers-of-interpreters)
  17. 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)
  18. 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)
  19. 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)
  20. 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)
  21. ⭐A SQL to C compiler in 500 lines of code (Journal of Functional Programming, 2019) by Tiark Rompf and Nada Amin
  22. 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)
  23. 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
  24. ⭐Collapsing Towers of Interpreters (POPL 2018) by Nada Amin and Tiark Rompf (Code: http://popl18.namin.net)
  25. ⭐Versatile Event Correlation with Algebraic Effects (ICFP 2018) by Oliver Bra\vcevac, Nada Amin, Guido Salvaneschi, Sebastian Erdweg, Patrick Eugster, and Mira Mezini
  26. ⭐LMS-Verify: Abstraction without Regret for Verified Systems Programming (POPL 2017) by Nada Amin and Tiark Rompf (Code: https://github.com/namin/lms-verify)
  27. ⭐Type Soundness Proofs with Definitional Interpreters (POPL 2017) by Nada Amin and Tiark Rompf (Code: http://popl17.namin.net)
  28. ⭐Type Soundness for Dependent Object Types (DOT) (OOPSLA 2016) by Tiark Rompf and Nada Amin (Code: http://oopsla16.namin.net)
  29. ⭐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
  30. ⭐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)
  31. ⭐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)
  32. ⭐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)
  33. 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)
  34. Computing with an SMT Solver (Tests and Proofs, 2014) by Nada Amin, K. Leino, and Tiark Rompf
  35. ⭐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
  36. 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
  37. 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
  38. Dafny for Metatheory of Programming Languages (2012) by Nada Amin (Code: https://github.com/namin/dafny-sandbox)
  39. 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)
  40. ⭐Scala-Virtualized: Linguistic Reuse for Deep Embeddings (Higher Order Symbol. Comput., 2012) by Tiark Rompf, Nada Amin, Adriaan Moors, Philipp Haller, and Martin Odersky
  41. ⭐JavaScript as an Embedded DSL (ECOOP 2012) by Grzegorz Kossakowski, Nada Amin, Tiark Rompf, and Martin Odersky (Code: https://github.com/js-scala)
  42. 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)
  43. ⭐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)
  44. ⭐Global architecture of genetic interactions on the protein network (Nat. Biotechnol., 2003) by Owen Ozier, Nada Amin, and Trey Ideker