SEmPE.md

Software Engineering meets Proof Engineering

Ideas from SE applied to maintanance of formal proofs.

Product lines of theorems and 3MT

A series of works by Benjamin Delaware and co-authors building frameworks of reusable components for building formalization of meta-theory from STLC and its variants.

• Product Lines of Theorems: a work exploring an idea of building a "product line" of PLs with different features, each requiring its own formalization.

• Meta-Theory a la Carte: Similar purpose, but build around Church encodings.

• Modular Monadic Meta-Theory: Adding extendable effects using monads.

Mining proofs patterns via Machine Learning

A series of works for identifying dulicating proofs and implementing corresponding refactorings:

• Machine Learning in Proof General: Interfacing Interfaces

• Proof-Pattern Recognition and Lemma Discovery in ACL2