Fully automatic modular theorem prover with code generation support
František Silváši, Martin Tomášek · 2017
We present a theorem prover capable of autonomously proving and subsequently synthesizing executable implementations of parameterized theorems. The overall design is modular, allowing for changes in source and target language, underlying calculus of deduction and proof construction strategies. We provide an example based on System F, with a custom specification language, Haskell target language and a heuristic strategy for proof inference. We also introduce an intermediate language for proof script representation, making the process of proof reconstruction trivial. Results are verified by generating a subset of Haskell's standard Prelude library, demonstrating that even systems without very expressive theoretical underpinnings (such as System F, or similar calculi) are sufficient for rudimentary proof/code inference.