Diese Dissertation zielt darauf ab, Typen als ein mächtiges Werkzeug für die Abstraktion in dem interaktiven Theorembeweiser Isabelle/HOL zu fördern. Der erste Beitrag ist die Lösung der offenen Frage, unter welchen Kriterien die Typen in Isabelle/HOL konsistent definiert werden können. Der zweite Beitrag ist die Entwicklung von Transfer und Lifting, Werkzeuge für den Aufbau von Bibliotheken abstrakter Typen (Subtypen oder Quotienten). Sie basieren auf den Begriffen von Reynolds relationaler Parametrizität und partiellen Quotienten.     «

Diese Dissertation zielt darauf ab, Typen als ein mächtiges Werkzeug für die Abstraktion in dem interaktiven Theorembeweiser Isabelle/HOL zu fördern. Der erste Beitrag ist die Lösung der offenen Frage, unter welchen Kriterien die Typen in Isabelle/HOL konsistent definiert werden können. Der zweite Beitrag ist die Entwicklung von Transfer und Lifting, Werkzeuge für den Aufbau von Bibliotheken abstrakter Typen (Subtypen oder Quotienten). Sie basieren auf den Begriffen von Reynolds relationaler Par...     »