Topics of GitHub Projects

topics(with count of selected projects): scheme17 paper-implementations15 reflection11 ai10 clojure7 scala7 towers7 generative-programming6 logic-programming6 minikanren6 binders5 llm5 common-lisp4 coq4 reasoning4 c3 collapsing-towers3 dafny3 meta-theory3 metaprogramming3 multi-stage-programming3 music3 oop3 racket3 synthesis3 constraints2 logic2 meta2 monte-carlo-tree-search2 ncats-translator2 prolog2 python2 truth-maintenance2 tutorial2 verification2

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 starting with FOL’78.

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