Topics of GitHub Projects

topics(with count of selected projects): scheme19 ai18 llm16 paper-implementations15 reflection13 dafny9 scala9 towers9 clojure8 generative-programming8 verification8 logic-programming7 minikanren7 metaprogramming6 binders5 coq5 synthesis5 collapsing-towers4 common-lisp4 lean4 meta-theory4 multi-stage-programming4 reasoning4 c3 constraints3 lemmascript3 logic3 monte-carlo-tree-search3 music3 oop3 prolog3 python3 racket3 reactjs3 tutorial3 ai-agents2 data-science2 discovery-system2 machine-learning2 meta2 ncats-translator2 proofsketcher2 smt2 talk2 truth-maintenance2 a-star-search1 abstract-interpretation1 analysis1 analytics1 argument-debugger1 chatgpt1 claude-code1 cli1 communication-bootstrapping1 compiler1 compiler-construction1 composition1 coq-formalization1 debate1 differentiable-programming1 docker1 expert-system1 fact-checking1 first-order-logic1 frama-c1 github1 harmony1 interactive1 interpreters1 java1 javascript1 jax1 jit1 jupyter1 jupyter-notebook1 jupyter-notebooks1 jupyterhub1 jupyterlab1 lean41 lisp1 mcp1 meta-reasoning1 metabolic-network1 neuro-symbolic1 ollama1 overtone1 plt-redex1 program-transformations1 react1 rocq1 theorem-prover1 twelf1 typescript1 unsound1 workshop1 x861

Current Research Projects

Verified Synthesis

generating and verifying programs and proofs using neurosymbolic programming and discovery systems, with targets in Dafny, Lean, Python & SMT

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

Drug Repurposing for Precision Medicine

led by the Hugh Kaul Precision Medicine Institute

Multi-stage miniKanren

multi-stage relational programming for fast synthesis from sketches

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.

Past Research Projects

Dependent Object Types (DOT)

EPFL: a type-theoretic foundation for languages like Scala

Lightweight Modular Staging (LMS)

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