E-Graphs, VSAs, and Tree Automata: a Rosetta Stone (EGRAPHS 2022) - PLDI 2022

Mon 13 - Fri 17 June 2022 San Diego, California, United States

Who

Yisu Remy Wang, James Koppel, Altan Haan, Josh Pollock

Track

Time Zone

The program is currently displayed in (GMT-07:00) Pacific Time (US & Canada).

Use conference time zone: (GMT-07:00) Pacific Time (US & Canada)Select other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

When

Tue 14 Jun 2022 11:15 - 11:30 at Toucan - Thinking Alike Chair(s): Max Willsey
Tue 14 Jun 2022 23:15 - 23:30 at Toucan - Thinking Alike

Abstract

Many tasks in programming languages involve representing and manipulating sets of programs. In program synthesis, the goal is to find a program satisfying a given specification from a set of programs possibly generated by a given grammar. In program optimization, the goal is to find an efficient program from the set of programs equivalent to the input. Programming languages research has considered various abstractions to represent sets of programs. Two examples are the version space algebra (VSA), popularized by FlashFill for enumerative program synthesis, and the e-graph that lies at the heart of an array of new program optimizers. In this talk we show that VSAs and e-graphs are but special cases of the well-studied finite-state (tree) automata from formal language theory. This new perspective allows us to place VSAs and e-graphs on a firm theoretical foundation, and also enables us to leverage powerful tools from formal language theory to perform tasks in programming languages. In the converse, bridging the concepts can also contribute to tree automata research with techniques developed for e-graphs and VSAs.

Link to Publication

https://docs.google.com/presentation/d/1oDNmzxJpsdLE51lmybcfzzzv4jRLDdrVpmMhMpFEoFk/edit?usp=sharing

Link to Preprint

https://remy.wang/reports/dfta.pdf

Yisu Remy Wang

University of Washington

United States

James Koppel

Massachusetts Institute of Technology, USA

Altan Haan

OctoML

Josh Pollock

MIT CSAIL

United States

Time Zone

The program is currently displayed in (GMT-07:00) Pacific Time (US & Canada).

Use conference time zone: (GMT-07:00) Pacific Time (US & Canada)Select other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Session Program

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