Interpretation of the Deductive Tableau in HOL
Abdelwaheb Ayari, David Basin · 1995
Our research investigates frameworks supporting the formalization of programming calculi and their application to deduction-based program synthesis. Here we report on a case study: within a conservative extension of higher-order logic implemented in the Isabelle system, we derived rules for program development which can simulate those of the deductive tableau proposed by Manna and Waldinger. We have used the resulting theory to synthesize a library of verified programs, focusing in particular on sorting algorithms. Our experience suggests that the methodology we propose is well suited both to implement and use programming calculi, extend them, partially automate them, and even formally reason about their correctness.