Towards Optimising Certified Programs by Proof Rewriting (EGRAPHS 2022) - PLDI 2022

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

Who

Kiran Gopinathan, Ilya Sergey

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:45 - 12:00 at Toucan - Thinking Alike Chair(s): Max Willsey
Tue 14 Jun 2022 23:45 - 00:00 at Toucan - Thinking Alike

Abstract

We present ongoing work on the use of e-graphs for the transformation of certified programs produced by a deductive synthesiser for heap-manipulating programs. We develop a strategy for optimising proofs using the mechanisms of e-graphs, propose a novel e-class analysis over \emph{proof scripts}, and report on its capabilities and limitations.

Kiran Gopinathan

National University of Singapore

Singapore

Ilya Sergey

National University of Singapore

Singapore

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