非表示:
キーワード:
-
要旨:
We report on a case study in using logical frameworks to support the
formalization of programming calculi and their application to
deduction-based program synthesis. Within a conservative extension of
higher-order logic implemented in the Isabelle system, we derived
rules for program development that 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 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.
