2021-07-30 –, Red
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.
Computer Science undergraduate student at the University of Pisa. Interested in functional programming, programming language theory, category theory, algebraic and symbolic computation, computability theory.
