From 25bddeb28bbcffd6a141e3371dc1c10821b4eba7 Mon Sep 17 00:00:00 2001
From: Marcus Rossel <marcusrossel@icloud.com>
Date: Tue, 16 Apr 2024 12:36:41 +0200
Subject: [PATCH] Add related work to README

---
 README.md | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 418b1ad..740a6c2 100644
--- a/README.md
+++ b/README.md
@@ -64,4 +64,9 @@ variable (and_assoc : ∀ a b c, (a ∧ b) ∧ c ↔ a ∧ (b ∧ c)) (and_idem
 
 example (h : p ∧ q ∧ r) : r ∧ r ∧ q ∧ p ∧ q ∧ r ∧ p := by
   egg [And.comm, and_assoc, and_idem] from h
-```
\ No newline at end of file
+```
+
+## Related Work
+
+* [Guided Equality Saturation](https://dl.acm.org/doi/10.1145/3632900) introduces the original prototype of the `egg` tactic.
+* [Bridging Syntax and Semantics of Lean Expressions in E-Graphs](https://github.com/marcusrossel/egraphs-2024/releases/tag/release) contains a high-level description of how the tactic handles binders and definitional equality. 
\ No newline at end of file