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 JunDisplayed time zone: Pacific Time (US & Canada) change
10:30 - 12:00 | |||
10:30 15mTalk | Logging an Egg: Datalog on E-Graphs EGRAPHS Philip Zucker Draper Laboratory Pre-print Media Attached | ||
10:45 15mTalk | Chasing an egg EGRAPHS Yihong Zhang University of Washington Pre-print | ||
11:00 15mTalk | 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 15mTalk | 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 15mTalk | Equality Saturation as a Tactic for Proof Assistants EGRAPHS | ||
11:45 15mTalk | Towards Optimising Certified Programs by Proof Rewriting EGRAPHS |
22:30 - 00:00 | |||
22:30 15mTalk | Logging an Egg: Datalog on E-Graphs EGRAPHS Philip Zucker Draper Laboratory Pre-print Media Attached | ||
22:45 15mTalk | Chasing an egg EGRAPHS Yihong Zhang University of Washington Pre-print | ||
23:00 15mTalk | 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 15mTalk | 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 15mTalk | Equality Saturation as a Tactic for Proof Assistants EGRAPHS | ||
23:45 15mTalk | Towards Optimising Certified Programs by Proof Rewriting EGRAPHS |