Types, Abstraction and Parametric Polymorphism in Higher-Order Logic

Kunčar, Ondřej

User: Guest

Ondřej Kunčar

If you experience problems opening the document, please try this link.

Original title:: Types, Abstraction and Parametric Polymorphism in Higher-Order Logic
Translated title:: Typen, Abstraktion und parametrischer Polymorphismus in Logik höherer Stufe
Author:: Kunčar, Ondřej
Year:: 2016
Document type:: Dissertation
Faculty/School:: Fakultät für Informatik
Advisor:: Nipkow, Tobias (Prof., Ph.D.)
Referee:: Nipkow, Tobias (Prof., Ph.D.); Paulson, Lawrence C. (Prof., Ph.D.)
Language:: en
Subject group:: DAT Datenverarbeitung, Informatik
TUM classification:: DAT 706d; DAT 540d
Abstract:: 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.
Translated abstract:: 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... »
WWW:: https://mediatum.ub.tum.de/?id=1285267
Date of submission:: 09.12.2015
Oral examination:: 08.04.2016
File size:: 1209905 bytes
Pages:: 172
Urn (citeable URL):: https://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:bvb:91-diss-20160408-1285267-1-5
Last change:: 12.07.2016
BibTeX