On a Strongly Normalizing STG Machine with an Application to Dependent Type Checking
| dc.contributor.advisor | Pepper, Peter | en |
| dc.contributor.author | Kleeblatt, Dirk | en |
| dc.contributor.grantor | Technische Universität Berlin, Fakultät IV - Elektrotechnik und Informatik | en |
| dc.date.accepted | 2011-03-16 | |
| dc.date.accessioned | 2015-11-20T20:21:08Z | |
| dc.date.available | 2011-04-14T12:00:00Z | |
| dc.date.issued | 2011-04-14 | |
| dc.date.submitted | 2011-04-14 | |
| dc.description.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. | de |
| dc.description.abstract | 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. | en |
| dc.identifier.uri | urn:nbn:de:kobv:83-opus-30165 | |
| dc.identifier.uri | https://depositonce.tu-berlin.de/handle/11303/3095 | |
| dc.identifier.uri | http://dx.doi.org/10.14279/depositonce-2798 | |
| dc.language | English | en |
| dc.language.iso | en | en |
| dc.rights.uri | http://rightsstatements.org/vocab/InC/1.0/ | en |
| dc.subject.ddc | 004 Datenverarbeitung; Informatik | en |
| dc.subject.other | Abhängige Typen | de |
| dc.subject.other | Compilerbau | de |
| dc.subject.other | Funktionale Sprachen | de |
| dc.subject.other | Verzögerte Auswertung | de |
| dc.subject.other | Compiler construction | en |
| dc.subject.other | Dependent types | en |
| dc.subject.other | Functional languages | en |
| dc.subject.other | Lazy evaluation | en |
| dc.subject.other | Strong normalization | en |
| dc.title | On a Strongly Normalizing STG Machine with an Application to Dependent Type Checking | en |
| dc.title.translated | Über eine vollständig normalisierende STG Maschine, mit einer Anwendung für die Prüfung abhängiger Typen | de |
| dc.type | Doctoral Thesis | en |
| dc.type.version | publishedVersion | en |
| tub.accessrights.dnb | free | * |
| tub.affiliation | Fak. 4 Elektrotechnik und Informatik::Inst. Softwaretechnik und Theoretische Informatik | de |
| tub.affiliation.faculty | Fak. 4 Elektrotechnik und Informatik | de |
| tub.affiliation.institute | Inst. Softwaretechnik und Theoretische Informatik | de |
| tub.identifier.opus3 | 3016 | |
| tub.identifier.opus4 | 2859 | |
| tub.publisher.universityorinstitution | Technische Universität Berlin | en |
Files
Original bundle
1 - 1 of 1