Unleashing Algebraic Metaprogramming in Julia with Metatheory.jl

07/30/2021, 1:00 PM1:30 PM UTC


A novel data structure and technique from theorem provers, a pattern matching system and classical term rewriting. Mix it with dynamism and the homoiconic metaprogramming system of Julia. Add algebraic composability. Shake well before using. What could go wrong? Composable compiler transforms, numerical code optimizers, interpreters and compilers, computer algebra systems, categorical theorem provers and much more to come. Come experiment with us and the Metatheory.jl package!


We introduce Metatheory.jl: a lightweight and performant general purpose symbolics and metaprogramming framework meant to simplify the act of writing complex Julia metaprograms and to significantly enhance Julia with a native term rewriting system, based on state-of-the-art equality saturation techniques, and a dynamic first class AST pattern matching system that is dynamically composable in an algebraic fashion, taking full advantage of the language’s powerful reflection capabilities. Our contribution allows performing general purpose symbolic mathematics, manipulation, optimization, synthesis or analysis of syntactically valid Julia expressions with a clean and concise programming interface, both during compilation or execution of programs. We have been currently experimenting with optimizing mathematical code and equational theorem proving strategies. This talk will discuss algebraic equational reasoning with examples from logic, program analysis, abstract algebra and category theory.

Platinum sponsors

Julia Computing

Gold sponsors

Relational AI

Silver sponsors

Invenia LabsConningPumas AIQuEra Computing Inc.King Abdullah University of Science and TechnologyDataChef.coJeffrey Sarnoff

Media partners

Packt Publication

Fiscal Sponsor