Benutzer: Gast  Login
Originaltitel:
Types, Abstraction and Parametric Polymorphism in Higher-Order Logic 
Übersetzter Titel:
Typen, Abstraktion und parametrischer Polymorphismus in Logik höherer Stufe 
Jahr:
2016 
Dokumenttyp:
Dissertation 
Institution:
Fakultät für Informatik 
Betreuer:
Nipkow, Tobias (Prof., Ph.D.) 
Gutachter:
Nipkow, Tobias (Prof., Ph.D.); Paulson, Lawrence C. (Prof., Ph.D.) 
Sprache:
en 
Fachgebiet:
DAT Datenverarbeitung, Informatik 
TU-Systematik:
DAT 706d; DAT 540d 
Kurzfassung:
This thesis aims to promote types as a powerful tool for abstraction in the interactive theorem prover Isabelle/HOL. The first contribution is having solved an open question under which criteria types can be defined consistently in Isabelle/HOL. The second contribution is development of Transfer and Lifting, tools providing automation for building libraries of abstract types (subtypes and quotients). They are based on notions of Reynolds's relational parametricity and partial quotients. 
Übersetzte Kurzfassung:
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...    »
 
Mündliche Prüfung:
08.04.2016 
Dateigröße:
1209905 bytes 
Seiten:
172 
Letzte Änderung:
12.07.2016