Proving Functional Program Equivalence via Directed Lemma Synthesis

Yican Sun, Ruyi Ji, Jian Fang +3

Proving equivalence between functional programs is a fundamental problem in program verification, which often amounts to reasoning about algebraic data types (ADTs) and composition…