Topics of GitHub Projects

topics(with count of selected projects): scheme17 paper-implementations15 ai14 reflection11 llm9 generative-programming8 scala8 towers8 clojure7 logic-programming6 minikanren6 binders5 coq5 synthesis5 collapsing-towers4 common-lisp4 dafny4 metaprogramming4 multi-stage-programming4 reasoning4 verification4 c3 constraints3 meta-theory3 music3 oop3 python3 racket3 data-science2 logic2 machine-learning2 meta2 monte-carlo-tree-search2 ncats-translator2 prolog2 smt2 truth-maintenance2 tutorial2

Current Research Projects

Verified Program Synthesis

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

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