Engelmann, Björn (2016) Techniques for the verification of dynamically typed programs. PhD, Universität Oldenburg.

- Accepted Version Volltext (7Mb)

Abstract

This thesis investigates the connection between static typing and program verification, or - phrased from the opposite direction - seeks to answer the question “why are there no verifiable, dynamically typed programming languages?”. We will demonstrate in this thesis that although common, the combination of static typing and program verification is not based on neccessity, but on convenience. To that end, we will define a dynamically typed programming language along with a program logic that we demonstrate to be both sound and (relative) complete, develop an approach to mitigate the overhead experienced during verification of dynamically typed programs, and finally combine static- and dynamic typing in a novel way, which enables deriving type safety guarantees for dynamically typed code without rewriting it into statically typed code and thereby generalizes both soft- and gradual typing.

["eprint_fieldname_title_plus" not defined]

Techniken zur Verifikation von dynamisch getypten Programmen

["eprint_fieldname_abstract_plus" not defined]

Diese Dissertation wird die Art der Verbindung zwischen statischen Typsystemen und Programmverifikation untersuchen. Es wird also der Frage nachgegangen, warum es keine verifizierbaren, dynamisch getypten Programmiersprachen gibt. Wir werden aufzeigen, dass die häufige Kombination aus statischem Typsystem und Programverifikation nicht auf Notwendigkeit beruht, sondern lediglich auf Bequemlichkeit. In diesem Sinne werden wir eine dynamisch getypte Programmiersprache und eine Programmlogik definieren, deren Korrektheit und (relative) Vollständigkeit beweisen, einen Ansatz entwickeln, den zusätzlichen Verifikationsaufwand bei dynamisch getypten Programmen zu reduzieren, und zu guter Letzt die statische und dynamische Typisierung auf eine neuartige Art kombinieren, die es ermöglicht, die Typ-Sicherheit von dynamisch getyptem Programmcode zu garantieren, ohne ihn in statisch getypten umschreiben zu müssen und dabei sowohl Soft- als auch Gradual-Typing generalisiert.

Item Type:	Thesis (PhD)
Uncontrolled Keywords:	Programmverifikation, Programmiersprache, Dynamische Typisierung, Formale Semantik, Hoare-Logik
Subjects:	Generalities, computers, information > Computer science, internet
Divisions:	School of Computing Science, Business Administration, Economics and Law > Department of Computing Science
Date Deposited:	21 Sep 2017 13:00
Last Modified:	09 Oct 2017 11:33
URI:	https://oops.uni-oldenburg.de/id/eprint/3288
URN:	urn:nbn:de:gbv:715-oops-33691
DOI:
Nutzungslizenz:

Actions (login required)

View Item