Ongoing Projects

• Extensible Models and Proofs (with Anastasiya Kravchuk-Kirilyuk, Jonas Iskander, Peter Chon, and Yizhou Zhang)

• Integration of formal verification into large language models

• 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, Mengjia Yan, Cameron Wong, Yuheng Yang, Muhammad Abdullah and Thomas Bourgeat)

• Generative Programming in Relational (Logic) Programming (with Michael Ballantyne, Raffi Sanna 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 metareflection.club. 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

• Relaxed machines: learning programs by gradient descent (joint work with Rob Zinkov)

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

• Semantics of staged relational programming [CS 152 or equivalent required]

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

• Dafny visualization (joint with Rustan Leino)

• 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) [FRAP or equivalent required]

• Auto-catalysis as reflection (with Walter Fontana) [CS + Chemistry required]

Supervised Projects

at Harvard

• Peter Chon (joint with Dimi Racordon), "Oxidize: A Step-Debugger for Static Semantics" 

• Will Dey, "QuTiE: Universal, Declarative, and Differentiable Physics Simulation"

• Ye Joo Han (co-supervised with Gennaro Chierchia), "Interpreting Language with Continuation-Based Semantics"

• Lavanya Singh (co-supervised with William Cochran), "Automated Kantian Ethics"

• Matthew Shabet, "An explanatory analysis of reaction-diffusion systems"

• Joey Velez-Ginorio (MIT), "Compositional desires as compositional programs"

• Lavanya Singh, "Three Implementations of the Categorical Imperative"

• Helena Abney-McPeek, "Domain-Specific Programming Language for Representing a Process for Music Composition"

• Laura Zharmukhametova, "microKanren with Delayed Goals"

• Marissa Zheng, "Investigating Migraine Treatments in mediKanren"

• Laura Zharmukhametova, "Explorations in miniKanren"

• Marissa Zheng, "Knowledge-Based Gene Ranking"

• Marissa Zheng, "mediKanren"

• Katherine Zhang, "mediKanren"

• Pratap Singh, “Dynamic Reflection”

• Teddy Liu, “A Type System for Multidimensional Arrays”

• Garrett Tanzer, “Programming “Programming by Example” by Example”

• Alex Wendland, “WebAssembly as a Multi-Language Platform”

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

• Ruben Fiszel, “Staged meta-programming, new LMS frontend and computation graphs”

• Samuel Grütter, “Connecting Scala to DOT”

• Fengyun Liu (co-supervised with Sandro Stucki), “Type-and-Effect Systems based on Capabilities”

• Fengyun Liu, “Dependency Resolution through SAT Solvers”

• Valérian Pittet, “Scala Music Generation”

• Samuel Grütter, “Machine-checked typesafety proofs”

• Daniel Espino, “Embedding Logical Frameworks in Scala”

• Samuel Grütter, “Explorations of Type Systems”