Tue 14 Jun 2022 10:45 - 11:00 at Toucan - Thinking Alike Chair(s): Max Willsey
Tue 14 Jun 2022 22:45 - 23:00 at Toucan - Thinking Alike

Recent years have seen a rejuvenation of e-graphs in many areas. However, the wide variety of e-graph applications is placing new requirements on the capability of e-graph frameworks, examples including multi-patterns and non-equational reasoning. To remedy these deficiencies, we need a radical change to the interfaces of existing e-graph frameworks like egg. We call the new interface design egg 2.0. What could egg 2.0 look like? Advances in e-graph and database researches give us some clues. In this talk, we argue that egg 2.0 should be based on the Datalog language, extended with data dependencies and the lattice semantics. We described egg­💡, a practical e-graph prototype built on top of SQLite with support for equality saturation. egg💡 exhibits some interesting designs and hints at the underlying connections between e-graphs and the chase, a fundamental algorithm in databases. Based on the experience with egg💡, we started a new design for egg 2.0, called egg#. We show how, besides the added expressivity, egg# can also potentially benefit from performance improvements from relational e-matching and semi-naive evaluations.

Tue 14 Jun

Displayed time zone: Pacific Time (US & Canada) change

10:30 - 12:00
Thinking AlikeEGRAPHS at Toucan +12h
Chair(s): Max Willsey University of Washington
10:30
15m
Talk
Logging an Egg: Datalog on E-Graphs
EGRAPHS
Philip Zucker Draper Laboratory
Pre-print Media Attached
10:45
15m
Talk
Chasing an egg
EGRAPHS
Yihong Zhang University of Washington
Pre-print
11:00
15m
Talk
ECTAs: E-Graphs Better (at Encoding)
EGRAPHS
James Koppel Massachusetts Institute of Technology, USA, Zheng Guo University of California, San Diego, Edsko de Vries Well-Typed LLP, Armando Solar-Lezama Massachusetts Institute of Technology, Nadia Polikarpova University of California at San Diego
11:15
15m
Talk
E-Graphs, VSAs, and Tree Automata: a Rosetta StoneVirtual
EGRAPHS
Yisu Remy Wang University of Washington, James Koppel Massachusetts Institute of Technology, USA, Altan Haan OctoML, Josh Pollock MIT CSAIL
Link to publication Pre-print
11:30
15m
Talk
Equality Saturation as a Tactic for Proof Assistants
EGRAPHS
Andrés Goens the University of Edinburgh, Siddharth Bhat the University of Edinburgh
11:45
15m
Talk
Towards Optimising Certified Programs by Proof Rewriting
EGRAPHS
Kiran Gopinathan National University of Singapore, Ilya Sergey National University of Singapore
22:30 - 00:00
Thinking AlikeEGRAPHS at Toucan
22:30
15m
Talk
Logging an Egg: Datalog on E-Graphs
EGRAPHS
Philip Zucker Draper Laboratory
Pre-print Media Attached
22:45
15m
Talk
Chasing an egg
EGRAPHS
Yihong Zhang University of Washington
Pre-print
23:00
15m
Talk
ECTAs: E-Graphs Better (at Encoding)
EGRAPHS
James Koppel Massachusetts Institute of Technology, USA, Zheng Guo University of California, San Diego, Edsko de Vries Well-Typed LLP, Armando Solar-Lezama Massachusetts Institute of Technology, Nadia Polikarpova University of California at San Diego
23:15
15m
Talk
E-Graphs, VSAs, and Tree Automata: a Rosetta StoneVirtual
EGRAPHS
Yisu Remy Wang University of Washington, James Koppel Massachusetts Institute of Technology, USA, Altan Haan OctoML, Josh Pollock MIT CSAIL
Link to publication Pre-print
23:30
15m
Talk
Equality Saturation as a Tactic for Proof Assistants
EGRAPHS
Andrés Goens the University of Edinburgh, Siddharth Bhat the University of Edinburgh
23:45
15m
Talk
Towards Optimising Certified Programs by Proof Rewriting
EGRAPHS
Kiran Gopinathan National University of Singapore, Ilya Sergey National University of Singapore