Merging Inductive Relations for Improved Program Specification

Explore a 19-minute video presentation from the PLDI 2023 conference on merging inductive relations. Delve into an algorithm for combining inductively defined properties that share an index, designed to improve the performance of automatic generation and simplify mechanized proofs. Learn how this approach finds shared structure between relations, creating a single merged relation equivalent to their conjunction. Discover the potential for orders of magnitude performance improvements in automatic generation and the elimination of nested induction and tedious book-keeping in proofs. Examine case studies demonstrating the algorithm's effectiveness and its implications for proof engineering tools like QuickChick. Gain insights into the power of inductive relations for writing program specifications and facilitating compositional reasoning in proof assistants.