The 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
  • Neuro-symbolic bijections
  • Modular verification
  • Reasoning over knowledge graphs
  • Joining relational programming and SMT (Satisfiability Modulo Theories) solving
  • Unifying probabilistic and constraint/logic programming
  • Automating (chip) design
  • Automating (biology) protocols

Programming Languages

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


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