Nada AMIN → Projects
 

Topics of GitHub Projects

topics^{_{(with count of selected projects)}}: scheme^₁₈ ai^₁₅ paper-implementations^₁₅ reflection^₁₂ llm^₁₀ scala^₉ clojure^₈ generative-programming^₈ towers^₈ logic-programming^₇ metaprogramming^₆ minikanren^₆ binders^₅ coq^₅ dafny^₅ synthesis^₅ verification^₅ collapsing-towers^₄ common-lisp^₄ meta-theory^₄ multi-stage-programming^₄ reasoning^₄ c^₃ constraints^₃ lean^₃ monte-carlo-tree-search^₃ music^₃ oop^₃ prolog^₃ python^₃ racket^₃ tutorial^₃ data-science^₂ discovery-system^₂ logic^₂ machine-learning^₂ meta^₂ ncats-translator^₂ proofsketcher^₂ smt^₂ talk^₂ truth-maintenance^₂ a-star-search^₁ abstract-interpretation^₁ chatgpt^₁ communication-bootstrapping^₁ compiler^₁ compiler-construction^₁ composition^₁ coq-formalization^₁ differentiable-programming^₁ docker^₁ expert-system^₁ frama-c^₁ github^₁ harmony^₁ interactive^₁ interpreters^₁ java^₁ jax^₁ jit^₁ lisp^₁ mcp^₁ meta-reasoning^₁ metabolic-network^₁ neuro-symbolic^₁ overtone^₁ plt-redex^₁ program-transformations^₁ rocq^₁ theorem-prover^₁ twelf^₁ unsound^₁ workshop^₁ x86^₁

Current Research Projects

Verified Program Synthesis

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

• VerMCTS
• OpenAI GPTs
• Dafny Sketcher
• Dafny Annotator
• Holey

Collapsing Towers for Side-Channel Security

at Harvard & MIT: 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

• code

Drug Repurposing for Precision Medicine

led by the Hugh Kaul Precision Medicine Institute

• mediKanren
• CHARM

Multi-stage miniKanren

multi-stage relational programming for fast synthesis from sketches

• code

Reflective Towers of Interpreters

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.

• SIGPLAN’21 blog post
• 80s & 90s
• Strange Loop Keynote ‘14
• POPL’18
• FOL’78

Past Research Projects

Dependent Object Types (DOT)

EPFL: a type-theoretic foundation for languages like Scala

• overview

Lightweight Modular Staging (LMS)

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

• LMS
• LMS-verify
• LMS Black