This thesis addresses two basic problems with the current crop of mechanized proof systems. The first problem is largely technical: the act of soundly introducing a recursive definition is not as simple and direct as it should be. The second problem is largely social: there is very little code-sharing between theorem prover implementations; as a result, common facilities are typically built anew in each proof system, and the overall progress of the field is thereby hampered. We use the application domain of functional programming to explore the first problem. We build a pattern-matching style recursive function definition facility, based on mechanically proven wellfounded recursion and induction theorems. Reasoning support is embodied by automatically derived induction theorems, which are customised to the recursion structure of definitions. This provides a powerful, guaranteed sound, definition-and-reasoning facility for functions that strongly resemble programs in languages such as ML or Haskell. We demonstrate this package (called TFL) on several well-known challenge problems. In spite of its power, the approach suffers from a low level of automation, because a termination relation must be supplied at function definition time. If humans are to be largely relieved of the task of proving termination, it must be possible for the act of defining a recursive function to be completely separate from the act of finding a termination relation for it and proving the ensuing termination conditions. We show how this separation can be achieved, while still preserving soundness. Building on this, we present a new way to define program schemes and prove high-level program transformations. Since the second problem is largely social, we cannot solve it alone; however, we do present an artifact that marks a path to a brighter future. In particular, we show that the sophisticated algorithms implemented in TFL can be parameterized by a higher order logic proof system. The package has been instantiated to HOL and Isabelle-HOL,two quite different mechanizations of higher order logic. In this exercise, we found that the fully formal approach taken to justifying definitions and deriving induction schemes was fundamental in providing the required combination of portability and soundness.
Übersetzte Kurzfassung:
Die vorliegende Doktorarbeit stellt eine parametrisierte Umgebung für die Entwicklung funktionaler Programme höhere Stufe innerhalb eines Beweissystems zur Verfügung. Die Umgebung wurde so entworfen, daß sie als korrekte Erweiterung für unterschiedliche Beweissysteme eingesetzt werden kann. Die Umgebung wird für zwei weiterhin genutzte Theorembeweiser installiiert.
Login
BibTeX