Research at the metareflection lab

The metareflection lab researches all aspects of static and dynamic reflection, programs / processes manipulating programs / processes.

Research Projects

• Theory (semantics) and practice (architectures, examples) of dynamic reflection
• Multi-stage programming to collapse levels of interpretation
• Applications of computational reflection to learning theories in cognitive science and psychology
• Mechanization of logic and meta-logic
• Architecture of neuro-symbolic computers
• Modular verification
• Reasoning over knowledge graphs
• Joining relational programming and SMT (Satisfiability Modulo Theories) solving
• Unifying probabilistic and constraint/logic programming
• Verified program synthesis
• PL/AI/LLMs for precision medicine, including drug repurposing
• Semi-interactive collaborative problem solving with LLMs

Programming Languages

• Coq, Lean
• SMTLIB, Dafny, Idris, F*
• Scala, OCaml, F#, SML
• miniKanren, Prolog
• Scheme, Common Lisp, Clojure
• Python
• C, Rust

Motto

• Hack for insights.
• Reflect to internalize.
• The rules of the game are part of the game.