Please use this identifier to cite or link to this item: http://dx.doi.org/10.14279/depositonce-2798
Main Title: On a Strongly Normalizing STG Machine with an Application to Dependent Type Checking
Translated Title: Über eine vollständig normalisierende STG Maschine, mit einer Anwendung für die Prüfung abhängiger Typen
Author(s): Kleeblatt, Dirk
Advisor(s): Pepper, Peter
Granting Institution: Technische Universität Berlin, Fakultät IV - Elektrotechnik und Informatik
Type: Doctoral Thesis
Language: English
Language Code: en
Abstract: Üblicherweise berechnen compilierte Programme lediglich sogenannte schwache Kopf-Normalformen. Allerdings benötigt man beispielsweise zur Überprüfung abhängiger Typen strenge Normalformen. Bei deren Berechnung müssen freie Variablen berücksichtigt werden, da z. B. formale Parameter von Abstraktionen frei in deren Rumpf auftreten können. Compilierter Maschinencode kann damit traditionell nicht umgehen. Dieses Problem durch den Einsatz eines Interpreters zu lösen bringt einige neue Probleme mit sich. - Die Ausführung von interpretiertem Code ist ineffizient. - Bei der Implementierung eines Compilers ist ein zusätzlicher Interpreter für die Typprüfung nötig, wodurch zwei Komponenten parallel gewartet werden müssen. - Unterschiedliche Resultate von Interpreter und Compiler können dazu führen, dass die Typsicherheit verletzt wird. Wir präsentieren ein strenges Normalisierungssystem für eine einfache funktionale Sprache mit verzögerter Auswertung, das diese Probleme durch den Einsatz von compiliertem Code vermeidet. Wir beginnen mit einer operationalen Semantik im deduktiven Stil, und transformieren sie schrittweise zu einer abstrakten Maschine, die Pseudo-Maschinencode ausführt. Dabei beweisen wir die Erhaltung von Normalformen. Mit einer Fallstudie belegen wir, dass sich das resultierende System tatsächlich für den Einsatz bei der abhängigen Typprüfung eignet, und dafür hinreichend effizient ist.
Traditionally, compiled systems compute so called weak head normal forms, i. e. they perform no computations beneath lambda-abstractions or case analyses. But for example in dependent type checking, strong normal forms are required to test for beta-convertibility. This requires to deal with free variables since e. g. formal parameters of abstractions occur free in the body of the abstraction, and compiled code usually cannot deal with this free variables. Using an interpreter solves this problem, but has several disadvantages: - Interpreted code has reduced performance compared to compiled code. - When writing a compiler, an additional interpreter is needed just for type checking, so, two different parts of the code base have to be maintained. - Differences between interpreter and compiler may result in computations having a different result at runtime than during type checking. This may violate type safety. We present a strong normalization system for FUN, a simple lazy functional language, that overcomes this disadvantages by using compiled code for normalization. We start with a big-step operational semantics, and transform it in several steps to an abstract machine executing pseudo-assembler code, thereby proving the preservation of normal forms. A case study confirms that the compilation system can be indeed used in a dependent type checker, and performs with a satisfying efficiency.
URI: urn:nbn:de:kobv:83-opus-30165
http://depositonce.tu-berlin.de/handle/11303/3095
http://dx.doi.org/10.14279/depositonce-2798
Exam Date: 16-Mar-2011
Issue Date: 14-Apr-2011
Date Available: 14-Apr-2011
DDC Class: 004 Datenverarbeitung; Informatik
Subject(s): Abhängige Typen
Compilerbau
Funktionale Sprachen
Verzögerte Auswertung
Compiler construction
Dependent types
Functional languages
Lazy evaluation
Strong normalization
Usage rights: Terms of German Copyright Law
Appears in Collections:Technische Universität Berlin » Fakultäten & Zentralinstitute » Fakultät 4 Elektrotechnik und Informatik » Institut für Softwaretechnik und Theoretische Informatik » Publications

Files in This Item:
File Description SizeFormat 
Dokument_9.pdf864.72 kBAdobe PDFThumbnail
View/Open


Items in DepositOnce are protected by copyright, with all rights reserved, unless otherwise indicated.