Towards Pen-and-Paper-Style Equational Reasoning in Interactive Theorem Provers by Equality Saturation

@article{rossel_popl26,
  author       = {Marcus Rossel and
                  Rudi Schneider and
                  Thomas Koehler and
                  Michel Steuwer and
                  Andr{\'{e}}s Goens},
  title        = {Towards Pen-and-Paper-Style Equational Reasoning in Interactive Theorem
                  Provers by Equality Saturation},
  journal      = {Proc. {ACM} Program. Lang.},
  volume       = {10},
  number       = {{POPL}},
  pages        = {718--747},
  year         = {2026},
  url          = {https://doi.org/10.1145/3776667},
  doi          = {10.1145/3776667},
  timestamp    = {Sun, 01 Feb 2026 00:00:00 +0100},
}