POPL preprint

Author: geezee

_bibliography/papers.bib

@@ -1,6 +1,32 @@
 ---
 ---
 
+@article{Zakhour:2025:Disequality,
+  acronym = {POPL},
+  projects = {Propel},
+  file = {papers/2025_Dis-Equality-Graphs.pdf},
+  author = {Zakhour, George and Weisenburger, Pascal and Cesario, Jahrim Grabriele and Salvaneschi, Guido},
+  title = {Dis/Equality Graphs},
+  year = {2025},
+  month = jun,
+  issue_date = {January 2025},
+  journal = {Proceedings of the ACM on Programming Languages},
+  volume = {8},
+  number = {POPL},
+  articleno = {77},
+  numpages = {24},
+  pages = {77:1--77:24},
+  location = {Denver, CO, USA},
+  publisher = {ACM},
+  address = {New York, NY, USA},
+  issn = {2475-1421},
+  doi = {10.1145/3704913},
+  keywords = {Automated Theorem Proving, E-Graphs, Disequalities},
+  supp = {https://zenodo.org/records/13938878},
+  abstract={E-graphs are a data structure to compactly represent a program space and reason about equality of program terms.  E-graphs have been successfully applied to a number of domains, including program optimization and automated theorem proving.  In many applications, however, it is necessary to reason about disequality of terms as well as equality.  While disequality reasoning can be encoded, direct support for disequalities increases performance and simplifies the metatheory.\par In this paper, we develop a framework independent of a specific implementation to formally reason about e-graphs.  For the first time, we prove the equivalence of e-graphs to the reflexive, symmetric, transitive, and congruent closure of the equivalence relation they are expected to encode.  We use these results to present the first formalization of an extension of e-graphs that directly supports disequalities and prove an analytical result about their superior efficiency compared to embedding techniques that are commonly used in SMT solvers and automated verifiers.  We further profile an SMT solver and find that it spends a measurable amount of time handling disequalities.\par We implement our approach in an extension to egg, a popular e-graph Rust library.  We evaluate our solution in an SMT solver and an automated theorem prover using standard benchmarks. The results indicate that direct support for disequalities outperforms other encodings based on equality embedding, confirming the results obtained analytically.},
+}
+
+
 @thesis{Sokolowski:2024:Reliable,
   type = {phdthesis},
   projects = {ProTI,µs},

_news/2024-11-14-popl-accpet.md

@@ -4,4 +4,4 @@ date: 2024-11-14
 inline: true
 ---
 
-Our paper 'Dis/Equality Graphs' accepted at POPL 2025, research track 🎉 Preprint coming soon.
+Our paper [Dis/Equality Graphs]({{ '/assets/pdf/papers/2025_Dis-Equality-Graphs.pdf' | relative_url }}){: target="_blank"} is accepted at [POPL '25](https://popl25.sigplan.org/){: target="_blank"}, research track 🎉 See you in Denver 🇺🇸

_pages/publications.md

@@ -3,7 +3,7 @@ layout: page
 permalink: /publications
 title: Publications
 description: Publications in reversed chronological order.
-years: [2024, 2023, 2022, 2021, 2020, 2019, 2018, 2017, 2016, 2015, 2014, 2013, 2012, 2011, 2010, 2009]
+years: [2025, 2024, 2023, 2022, 2021, 2020, 2019, 2018, 2017, 2016, 2015, 2014, 2013, 2012, 2011, 2010, 2009]
 nav: true
 nav_rank: 4
 ---