Ongoing Projects

  • Extensible Models and Proofs (with Anastasiya Kravchuk-Kirilyuk and Yizhou Zhang)

  • Drug Repurposing via Causality and Truth-Maintenance Systems (with William Byrd, Jeremy Zucker, Michael Patton, Marissa Zheng and many others at the Hugh Kaul Precision Medicine Institute in Alabama and the Pacific Northwest National Laboratory)

  • Collapsing Towers for Side-Channel Security (with Adam Chlipala and Thomas Bourgeat)

  • Generative Programming in Relational (Logic) Programming (with Michael Ballantyne and William Byrd)

  • Reflective Meta-Level Architectures

  • A Neural Compiler (with Joey Velez-Ginorio)

  • CLP(SMT) (with Siyuan Chen, Michael Ballantyne, William Byrd)

For a list of general current directions, see the list on In addition, our list of publications gives an idea of recent and past work. See also our partial list of code. Finally class projects from CS252R are a good initial source for research projects. 

Potential Joint Projects

If you're interested in any of these, please contact me.

  • Self-Optimizing Network Functions (joint with Minlan Yu)

  • Programming Microfluidics (joint with Saman Amarasinghe)

  • miniKanren in Agda (joint with Jason Hemann)

  • Semantics of staged relational programming (joint with Jason Hemann) [CS 152 or equivalent required]

  • miniKanren search visualization and exploration (joint with William Byrd)

  • Dafny visualization (joint with Rustan Leino)

  • Hoare's Geometric Theory of Program Testing (joint with Sir Tony Hoare)

  • Proving Decentralized Applications Secure (joint with François-René Rideau)

  • Step debugger for Rust’s type system (joint with Dimitri Racordon) [CS 152 or equivalent required]

  • Functional/Logical Type-checking of Traits in Rust (joint with Niko Matsakis)

  • Generative Verification Case Study: RE to NFA to DFA to C/Assembly (with Adam Chlipala and Clément Pit-Claudel)

Blue-Sky Projects for Undergraduates (possibly Senior Theses)

  • Abstracting from writing systems into the common language of phonetics

I am also open to brainstorming ideas.

Supervised Projects

at Harvard

at Cambridge, UK

  • Michael Buch (co-supervised with Alan Mycroft), “Collapsing Heterogenous Towers of Interpreters”

  • Yan Han (co-supervised with Neel Krishnaswami), “Analyzing Music with Prefix Trees”

  • Niall Engan, “A Domain-Specific Language for Image Processing Pipelines”

  • Joey Velez-Ginorio (Oxford) (co-supervised with Daniel Kroening), "Learning in System F"

at EPFL, Switzerland