Nada Amin's CV

Papers

‘‘Persimmon: Nested Family Polymorphism with Extensible Variant Types’’, Anastasiya Kravchuk-Kirilyuk, Gary Feng, Jonas Iskander, Yizhou Zhang, & Nada Amin, Proceedings of the ACM on Programming Languages (OOPSLA), April 2024
‘‘LURK: Lambda, the Ultimate Recursive Knowledge (Experience Report)’’, Nada Amin, John Burnham, François Garillot, Rosario Gennaro, Chhi’mèd Künzang, Daniel Rogozin, & Cameron Wong, Proceedings of the ACM on Programming Languages (ICFP), August 2023
‘‘The Dolorem Pattern: Growing a Language Through Compile-Time Function Execution’’, Simon Henniger & Nada Amin, In 37th European Conference on Object-Oriented Programming (ECOOP 2023), July 2023
‘‘Extensible Metatheory Mechanization via Family Polymorphism’’, Ende Jin, Nada Amin & Yizhou Zhang, Proceedings of the ACM on Programming Languages (PLDI), June 2023
‘‘Reasoning about ‘‘Reasoning about Reasoning’’: Semantics and Contextual Equivalence for Probabilistic Programs with Nested Queries and Recursion’’, Yizhou Zhang & Nada Amin, Proceedings of the ACM on Programming Languages 6 (POPL), January 2022
‘‘Prototypes: Object-Orientation, Functionally’’, François-René Rideau, Alex Knauth, & Nada Amin, Scheme and Functional Programming Workshop, August 2021
‘‘Prolog-Style Meta-Programming miniKanren’’, Nada Amin, William E. Byrd, & Tiark Rompf, miniKanren and Relational Programming Workshop, August 2021
‘‘Technical Perspective: Programming Microfluidics to Execute Biological Protocols’’, Nada Amin, Communications of the ACM, February 2021
‘‘mediKanren: a System for Biomedical Reasoning’’, William E. Byrd, & al., miniKanren and Relational Programming Workshop, August 2020
‘‘Lightweight Functional Logic Meta-Programming’’, Nada Amin, William E. Byrd, & Tiark Rompf, APLAS'19: Programming Languages and Systems, December 2019 (code)
‘‘A SQL to C Compiler in 500 Lines of Code’’, Tiark Rompf & Nada Amin, Journal of Functional Programming, June 2019
‘‘Versatile Event Correlation with Algebraic Effects’’, Oliver Bracevac, Nada Amin, Guido Salvaneschi, Sebastian Erdweg, Patrick Eugster, & Mira Mezini, Proceedings of the ACM on Programming Languages 2 (ICFP), August 2018
‘‘Collapsing Towers of Interpreters’’, Nada Amin & Tiark Rompf, Proceedings of the ACM on Programming Languages 2 (POPL), January 2018 (code)
‘‘LMS-Verify: Abstraction without Regret for Verified Systems Programming’’, Nada Amin & Tiark Rompf, POPL'17: 44th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, January 2017 (code)
‘‘Type Soundness Proofs with Definitional Interpreters’’, Nada Amin & Tiark Rompf, POPL'17: 44th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, January 2017 (code)
‘‘Type Soundness for Dependent Object Types’’, Tiark Rompf & Nada Amin, OOPSLA'16: 31st ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications, November 2016 (code)
‘‘Java and Scala's Type Systems are Unsound: The Existential Crisis of Null Pointers’’, Nada Amin & Ross Tate, OOPSLA'16: 31st ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications, November 2016 (code)
‘‘The Essence of Dependent Object Types’’, Nada Amin, Samuel Grütter, Martin Odersky, Tiark Rompf & Sandro Stucki, A List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday, April 2016 (code)
‘‘Functional Pearl: A SQL to C Compiler in 500 Lines of Code’’, Tiark Rompf & Nada Amin, ICFP'15: 20th ACM SIGPLAN International Conference on Functional Programming, August 2015 (code)
‘‘Foundations of Path-Dependent Types’’, Nada Amin, Tiark Rompf & Martin Odersky, OOPSLA'14: 29th ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications, October 2014 (code)
‘‘Computing with an SMT solver’’, Nada Amin, Rustan Leino & Tiark Rompf, TAP'14: 8th International Conference on Tests & Proofs, July 2014
‘‘Scala-virtualized: Linguistic reuse for deep embeddings’’, Tiark Rompf et al., HOSC: Higher Order and Symbolic Computation, 2013 (code)
‘‘What are the Odds?: probabilistic programming in Scala’’, Sandro Stucki, Nada Amin, Manohar Jonnalagedda & Tiark Rompf, Scala'13, July 2013 (code)
‘‘A Flow-Insensitive, Modular Effect System for Purity’’, Lukas Rytz, Nada Amin & Martin Odersky, FTfJP'13: Formal Techniques for Java-like Programs, July 2013
‘‘Optimizing Data Structures in High-Level Programs’’, Tiark Rompf et al., POPL'13: 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, January 2013
‘‘Dependent Object Types’’, Nada Amin, Adriaan Moors & Martin Odersky, FOOL'12: 19th International Workshop on Foundations of Object-Oriented Languages, October 2012 (code)
‘‘JavaScript as an Embedded DSL’’, Grzegorz Kossakowski, Nada Amin, Tiark Rompf & Martin Odersky, ECOOP'12: 26th European Conference on Object-Oriented Programming, June 2012 (code)
‘‘Computer-Aided Design for Microfluidic Chips Based on Multilayer Soft Lithography’’, Nada Amin, William Thies & Saman Amarasinghe, ICCD'09: IEEE International Conference on Computer Design, October 2009 (site)
‘‘Cytoscape: A Software Environment for Integrated Models of Biomolecular Interaction Networks’’, Paul Shannon et al., Genome Research, November 2003; 13: 2498-2504 (site)
‘‘Global architecture of genetic interactions on protein network’’, Owen Ozier, Nada Amin & Trey Ideker, Nature Biotechnology, May 2003;21(5):490-1 (site)

Talks and Meetings

IFIP WG2.11 (Working Group on Program Generation), Philadelphia, PA, March 25 to 28, 2024.
IFIP WG2.16 (Working Group on Language Design), Pittsburgh,PA, March 4 to 8, 2024
‘‘Staged Relational Programming for Synthesis’’ (with William Byrd), AP2S: Automated Program and Proof Synthesis Bridge Program, Part of the AAAI-23 Bridge Program, February 7, 2023.
‘‘Systems Programming’’, Lorentz center workshop on new challenges in programming language semantics, Leiden, Netherlands, November 28, 2022.
‘‘Staged Relational Interpreters: Running with Holes, Faster’’, IFIP WG2.11 (Working Group on Program Generation), Odense, Denmark, August 16, 2022
‘‘Reconciling Family Polymorphism with Pattern Matching via Extensible Cases’’, IFIP WG2.16 (Working Group on Language Design), March 8, 2022
‘‘Programming Languages + Artificial Intelligence’’, Museum of Science (Science Live!), February 23, 2022
‘‘Beyond Collapsing Towers: Staging a Relational Interpreter’’, Northeastern University, October 29, 2021
‘‘Beyond Collapsing Towers: Staging a Relational Interpreter’’, Boston University (Principles of Programming & Verification Seminar), October 26, 2021
‘‘Prolog-Style Meta-Programming miniKanren’’ (with William Byrd), miniKanren and Relational Programming Workshop, August 26, 2021
‘‘Adventures in extending miniKanren’’, keynote at miniKanren and Relational Programming Workshop, August 26, 2021
‘‘Staged Relational Interpreters: Running Backwards, Faster’’, keynote at European Lisp Symposium (ELS), May 4, 2021
‘‘Functional Programming for COVID-19 Drug Repurposing’’, (PLMW), ICFP, August 23, 2020
IFIP WG2.8 (Working Group on Functional Programming), Bordeaux, France, May 20 — 24, 2019
‘‘Generating C from Scala’’, invited seminar at University of Leicester, Uk, October 26, 2018
‘‘Generating C from Scala’’, invited seminar at University City London (UCL), Uk, October 5, 2018
Heidelberg Laureate Forum, per invitation of Sir Tony Hoare, Germany, September 23 — 29, 2018
‘‘CLP(SMT)’’, Invited Talk at ClojuTRE, Helsinki, Finland, September 14, 2018
IFIP WG2.8 (Working Group on Functional Programming), Asilomar, Ca, Usa, June 10 — 15, 2018
NII Shonan Meeting Seminar on Meta-Programming for Statistical Machine Learning, Japan, May 21 — 25, 2018
IFIP WG2.16 (Working Group on Language Design), Antwerp, Belgium, May 14-18, 2018
‘‘Hands-on Generative Programming: Write an Interpreter, Build a Compiler’’, Invited Talk at PLAS seminar, University of Kent, Canterbury, Uk, November 20, 2017
‘‘Collapsing Towers of Interpreters’’, codemesh.io, London, Uk, November 8, 2017
‘‘Collapsing Towers of Interpreters’’, Invited Talk at Meta (Workshop on Meta-Programming Techniques and Reflection), SPLASH, Vancouver, bc, Canada, October 22, 2017
‘‘DOT: Scala Types in Theory and Practice’’, Scala.World, Penrith, Uk, September 18, 2017
‘‘Scala: Types in Theory and Practice’’, Programming Language Mentoring Workshop (PLMW), ICFP, Oxford, Uk, September 3, 2017
IFIP WG2.16 (Working Group on Language Design), Park City, Ut, Usa, August 28 — September 1, 2017
‘‘Generative Programming & Verification’’, Keynote at EuroClojure, Berlin, Germany, July 21, 2017
‘‘Collapsing Towers of Interpreters’’, IFIP WG2.11 (Working Group on Program Generation), Koblenz, Germany, July 18, 2017
‘‘Types: Safety Net & Springboard’’, Invited Talk
- Aarhus University, Denmark, April 10, 2017
- Microsoft Research, Cambridge, Uk, March 30, 2017
- USI, Lugano, Switzerland, March 27, 2017
- Microsoft Research, Redmond, Wa, Usa, March 21, 2017
- University of Cambridge, Uk, March 16, 2017
- Harvard University, Cambridge, Ma, Usa, March 9, 2017
- ETH Zürich, Switzerland, March 7, 2017
- UCLA, Los Angeles, Ca, Usa, February 28, 2017
‘‘The cake and eating it: writing expressive high-level programs that generate fast low-level code at runtime’’, Kats Conf 2, Dublin, Ireland, February 18, 2017
‘‘Thinking About Recursion’’ (with William Byrd), Kats Conf 2, Dublin, Ireland, February 17, 2017
Theory and Applications of Behavioural Types, Dagstuhl Seminar 17051, Germany, January 29 — February 3, 2017
‘‘LMS-Verify: Abstraction Without Regret for Verified Systems Programming’’, POPL, Paris, France, January 20, 2017
Panel of Young Researchers, Programming Language Mentoring Workshop (PLMW), POPL, Paris, France, January 17, 2017
‘‘Type Soundness for Dependent Object Types (DOT)’’, OOPSLA, Amsterdam, Netherlands, November 3, 2016
Panel of Young Researchers, Programming Language Mentoring Workshop (PLMW), SPLASH, Amsterdam, Netherlands, November 1, 2016
‘‘Generative Programming: from High-Performance to Safety-Critical Applications’’, Invited Talk at Mobile!, Amsterdam, Netherlands, October 31, 2016
‘‘LMS: Generative Programming in Scala’’, EPFL - Novi Sad SCOPES meeting, Lausanne, Switzerland, June 29, 2016
‘‘The DOT Calculus’’, ECOOP PC Workshop, Brown University, Providence, Ri, Usa, February 28, 2016
IFIP WG2.16 (Working Group on Language Design), UCLA, Los Angeles, Ca, Usa, January 25 — 29, 2016
‘‘LMS: a Perspective on Generative Programming’’, Invited Talk at PEPM, St Petersburg, Fl, Usa, January 18, 2016
‘‘Programming should eat itself’’, Keynote at Strange Loop, St Louis, Mo, Usa, September 19, 2014 (code)
‘‘Batteries Included: Generative Programming with Scala and LMS’’ (with Tiark Rompf), Tutorial at CUFP, Gothenburg, Sweden, September 5, 2014
‘‘Implicits in Practice’’ (with Tiark Rompf), Demo at ML Family Workshop, Gothenburg, Sweden, September 4, 2014
‘‘The DOT Calculus’’, Scala Days, Berlin, Germany, June 18, 2014
‘‘Patterns for Generative Programming’’, EcoCloud Annual Event, Lausanne, Switzerland, June 6, 2014
NII Shonan Meeting Seminar on Staging and High-Performance Computing, Japan, May 26 — 30, 2014
‘‘The DOT Calculus’’, flatMap(Oslo), Norway, May 12, 2014
‘‘Mind the Gap’’ (with Tiark Rompf), OBT 2014, San Diego, Ca, Usa, January 25, 2014
‘‘Meta-Programming in Logic Programming’’ (with William Byrd), codemesh.io, London, Uk, December 5, 2013 (code)
‘‘From Greek to Clojure!’’ (with William Byrd), Clojure/conj, Alexandria, Va, Usa, November 14, 2013 (code)
‘‘Program Transformations’’ (with William Byrd), Hacker School (Recurse Center), New York, Ny, Usa, July 22, 2013
‘‘Staging: Runtime code generation for ‘abstraction without regret’’’, Hacker School (Recurse Center), New York, Ny, Usa, July 15, 2013
‘‘Program Transformations’’ (with William Byrd), LambdaJam, Chicago, Il, Usa, July 9, 2013 (code)
‘‘How to write your next POPL paper in Dafny’’, Microsoft Research, Redmond, Wa, Usa, July 2, 2013 (code)
‘‘Lightweight Modular Staging’’ (with Tiark Rompf et al.), Tutorial at PLDI, Seattle, Wa, Usa, June 16, 2013
‘‘core.logic.nominal’’, miniKanren Confo (associated with Clojure/West), Portland, Or, Usa, March 19, 2013 (code)
‘‘Dependent Object Types’’, FOOL, Tucson, Az, USA, October 22, 2012
Participant at the Oregon Programming Languages Summer School (OPLSS), Eugene, Or, Usa, July 16-28, 2012
‘‘JavaScript as an Embedded DSL’’, ECOOP, Beijing, China, June 15, 2012
‘‘JavaScript as an Embedded DSL’’, Scala Days, London, Uk, April 17, 2012

Education

Ecole Polytechnique Fédérale de Lausanne (l'EPFL)

Lausanne, VD, Switzerland

2011

2016

Doctoral Program in Computer, Communication and Information Sciences
Thesis: Dependent Object Types
Coursework includes
- Foundations of Software [Scala]
- Synthesis, Analysis, Verification [Scala]
Teaching assistant for Functional Programming Principles in Scala (2012, 2013, 2014), Principles of Reactive Programming (2013)
Teaching assistant for Programming I in Environmental Sciences & Engineering (2013), in Microengineering and in Electrical & Electronics Engineering (2015)
‘‘Teaching Assistant Team Award’’ for Programming I (2015)

Massachusetts Institute of Technology (MIT)

Cambridge, Ma, Usa

Fall 2001

Fall 2008

Master of Engineering in Electrical Engineering & Computer Science, December '08
Thesis: Computer-Aided Design for Multilayer Microfluidic Chips
Bachelor of Science in Computer Science & Engineering with Music Minor, May '08 — advised by Prof. M. Frans Kaashoek
Coursework included
- Computer System Architecture [Assembly, C++] (G)
- Large-scale Symbolic Systems [Scheme, Common Lisp] (G+)
- Advanced Algorithms (G)
- Multithreaded Parallelism: Languages and Compilers [Haskell] (G~)
- Computational Biology [Python] (G~)
- Classical Mechanics: A Computational Approach [Scheme] (G)
- Audio Processing by People and Machines [Csound] (G)
- Fundamentals of Probability (G)
- Laboratory in Software Engineering [Java]
- Computer Systems Engineering
- Microcomputer Project Laboratory [Assembly]
- Signals & Systems [Matlab]
- Introduction to Algorithms
- Mathematics for Computer Science
- Circuits & Electronics
- Structure & Interpretation of Computer Programs [Scheme]
- Information & Entropy
- Introduction to Western Music
- Harmony & Counterpoint I & II
- MIT Concert Choir
- American Music (~)
- Film Music
- Modern Fiction
- Introduction to Linguistics (+)
Lab assistant & tutor for 6.001 Structure & Interpretation of Computer Programs (2004, 2005, 2006)
Tutor for 6.046 Introduction to Algorithms (2005)
6.170 Letter of Commendation awarded by Prof. Michael Ernst for outstanding performance in the ‘‘Laboratory in Software Engineering’’ class (2005)

Ecole Polytechnique Fédérale de Lausanne (l'EPFL)

Lausanne, VD, Switzerland

Spring 2004 & Spring 2007

Teaching assistant for Prof. Wulfram Gerstner's master-level machine learning course
Independent studies as a free-moving students
Coursework included
- Artificial Intelligence [Common Lisp]
- Natural Language Processing [C++]
- Artificial Neural Networks [C, Python]
- Bio-Inspired Adaptive Machines [C, Python]
- Bioinformatics
- Modern Abstract Algebra
- Linear Algebra
- Economics

Ecole Polytechnique (l'X)

Palaiseau, France

Fall 2003

Exchange student
Coursework included
- Computer Architecture
- Automata, Computability, and Complexity
- Programming Languages [OCaml]
- Computer Graphics [C++]
Part of the school's all-girls basketball team

Collège Rousseau

Geneva, GE, Switzerland

August 1997

June 2001

Maturité cantonale et fédérale mention ‘‘bien’’

Industry

Google

Zürich, Switzerland

2009

2011

Gmail Software Engineer
Projects included
- Compiler infrastructure supporting Gmail and Google Apps
- Tools to diagnose Gmail's latency
- Reducing server-side latency of sending emails
- Reducing client-side latency of initial loading
- Reducing lockouts of legitimate Gmail users
- Prototyping a Wave / Gmail integration lab, launched internally
Code in Java, JavaScript, Python, Sawzall, Dremel, Awk & shell scripts
Awarded a Peer Bonus for enabling usage of Gmail's CSS compiler for Android projects
Part of the performance team that reduced stylesheet compilation from 5% of total cluster CPU time of Gmail to negligible
Trained on the Gmail release cycle, finding a bug initially classified as a cosmic ray

Google

Zürich, Switzerland

Summer 2008

Intern Software Engineer
Improved type inference and checking in a JavaScript-to-JavaScript compiler performing static analysis, code optimization and code compression
Awarded a Peer Bonus for "benefiting numerous projects including all of Google Apps"
See the Closure Compiler, opensourced in November 2009

Microsoft

Redmond, Wa, Usa

Summer 2006

Intern Software Development Engineer
Extended Visual Studio in C# to enable a RAD (Rapid-Application Development) experience for data-driven WCF (Windows Communication Foundation) clients

Lombard Odier Darier Hentsch (Private Bankers)

Geneva, Switzerland

Summer 2004

Intern in IT Architecture
Developed a solution to authenticate network devices with disconnected smartcard readers in C++ according to the RADIUS standard

ArsDigita Foundation

Cambridge, Ma, Usa

Summer 2000

Built & maintained database-backed websites using Oracle's RDBMS with Philip Greenspun
Instructed software engineers on web services
Toured California as part of a non-profit organization to match pet lovers with abandoned pets
First runner-up in ArsDigita Prize 1999 for Metis Service

Nada AMIN

Harvard John A. Paulson School of Engineering and Applied Sciences (SEAS)

Research

Papers

Talks and Meetings

Professional Service

Department of Computer Science & Technology, University of Cambridge

Software Technology Group, TU Darmstadt

Programming Methods Laboratory, LAMP, EPFL

RiSE, Microsoft Research

Computer Architecture Group, Computer Science & Artificial Intelligence Laboratory

Computational Molecular Biology, Max-Planck Institute for Molecular Genetics

Supercomputing Technologies Group, Laboratory for Computer Science

Ideker Lab, Whitehead Institute for Biomedical Research

Education

Ecole Polytechnique Fédérale de Lausanne (l'EPFL)

Massachusetts Institute of Technology (MIT)

Ecole Polytechnique Fédérale de Lausanne (l'EPFL)

Ecole Polytechnique (l'X)

Collège Rousseau

Industry

Google

Google

Microsoft

Lombard Odier Darier Hentsch (Private Bankers)

ArsDigita Foundation