Footnote:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Description:
In order to allow for the verification of realistic problems, Coq provides a languagefor tactic programming, therefore enabling general-purpose scripting of automation routines. However, this language is untyped, and as a result, tactics are known to be difficult to compose, debug, and maintain. In this thesis, I develop two different approaches to typed tactic programming in the context of Coq: Lemma Overloading and Mtac. The first one utilizes the existing mechanism of overloading, already incorporated into Coq, to build typed tactics in a style that resembles that of dependently typed logic programming. The second one, Mtac, is a lightweight yet powerful extension to Coq that supports dependently typed functional tactic programming, with additional imperative features. I motivate the different characteristics of Lemma Overloading and Mtac through a wide range of examples, mainly coming from program verification. I also show how to combine these approaches in order to obtain the best of both worlds, resulting in extensible, typed tactics that can be programmed interactively. Both approaches rely heavily on the unification algorithm of Coq, which currently suffers from two main drawbacks: it incorporates heuristics not appropriate for tactic programming, and it is undocumented. In this dissertation, in addition to the aforementioned approaches to tactic programming, I build and describe a new unification algorithm better suited for tactic programming in Coq. ; Um realistische Programme zu verifizieren, bietet Coq eine Sprache zum Programmieren von Taktiken. Sie ermöglicht das Schreiben universeller Automatisierungsroutinen. Diese Sprache ist allerdings ungetypt. Die resultierenden Taktiken sind daher bekannt dafür, schwer zusammensetzbar, testbar und wartbar zu sein. Ich entwickle in dieser Doktorarbeit zwei Ansätze für getypte Taktiken im Kontext von Coq: Das Überladen von Lemmata und Mtac. Ersteres benutzt den in Coq vorhandenen Überladungsmechanismus um Taktiken im Stil von Dependently Typed Logic ...