On a Strongly Normalizing STG Machine with an Application to Dependent Type Checking [Elektronische Ressource] / Dirk Kleeblatt. Betreuer: Peter Pepper

Dirk Kleeblatt

Sujets

• Informatik

Informations

• Publié par: technische_universitat_berlin
• Publié le: 01 janvier 2011
• Nombre de lectures: 5
• Langue: English

Extrait

D I R K K L E E B L AT T
OnaStronglyNormalizingSTGMachine
With an Application to Dependent Type CheckingD I R K K L E E B L AT T
Von der Fakultät IV – Elektrotechnik und Informatik –
der Technischen Universität Berlin
zur Erlangung des akademischen Grades
Doktor der Ingenieurwissenschaften – Dr.-Ing. –
genehmigte Dissertation
vorgelegt von
Diplom-Ingenieur Dirk Kleeblatt aus Berlin
Promotionsausschuss:
Prof. Dr. rer. nat. Sabine Glesner (Vorsitzende)
Prof. Dr. rer. nat. Peter Pepper (Erster Gutachter)
Prof. Dr. rer. nat. Petra Hofstedt (Zweite Gutachterin)
Tag der wissenschaftlichen Aussprache: 16. März 2011
Berlin, 2011
D 83
OnaStronglyNormalizingSTGMachine
With an Application to Dependent Type CheckingC O N T E N T S
i introduction 9
1 motivation 11
1.1 Dependent Types 11
1.2 Normalization 13
1.3 Nor for Dependent Type Checking 15
1.3.1 Dependently typed languages 15
1.3.2 Proof Assistants Based on Dependent Types 16
1.4 Laziness 18
1.5 Goal of This Thesis 19
1.6 Outline 20
2 state of the art 23
2.1 The Strongly Normalizing zam 23
2.2 The Strongly Nor Machine k 23
2.3 Theπ-Red System 24
2.4 Normalization by Evaluation 25
2.4.1 Typed Normalization by Evaluation 25
2.4.2 Untyped Nor by Ev 26
ii normalization using compiled code 29
3 definition of the semantics: s4 31
3.1 Language Syntax 32
3.2 Normal Forms 33
3.3 Heaps and Accumulators 35
3.4 Normalizing fun expressions 36
3.5 Evaluation to whnf 37
3.6 Read Back 40
3.7 Example 41
3.8 Well-formedness 43
4 linearization: sstg1 45
4.1 Stacks and Heaps 45
4.2 Weak Evaluation 46
4.3 Normalization and Read Back 48
4.4 Heap Correspondence 50
4.5 Equivalence of s4 and sstg1 51
4.5.1 Completeness 51
4.5.2 Soundness 52
4.5.3 Correctness 53
5 introduction of closures: sstg2 55
5.1 Modifications of the Syntax 55
5.2 Environments 57
5.3 Normalization 57
5.4 Equivalence of sstg1 and sstg2 59
5Contents
6 compiling to machine code: isstg 63
6.1 An Execution Environment for isstg 63
6.2 Compilation and Weak Evaluation 65
6.2.1 Compilation of Applications 67
6.2.2 of Local Bindings 67
6.2.3 of Case Discriminations 69
6.2.4 Preallocated Code Sequences 70
6.3 Strong Normalization and Read Back 71
6.4 Correspondence Between sstg2 and isstg 71
6.5 Equivalence of sstg2 and isstg 75
6.6 Correctness of Compiled Normalization 77
iii dependent type checking 79
7 pure type systems 81
7.1 Basic Typing Rules 81
7.1.1 Syntax 82
7.1.2 Typing 83
7.1.3 Example: The Calculus of Constructions 85
7.2 Inductive Data Types 86
7.2.1 Syntax 87
7.2.2 Typing 87
7.2.3 Examples 88
7.3 Case Analyses 90
7.3.1 Syntax 91
7.3.2 Typing 91
7.3.3 Examples 92
7.4 Definitions by Fixed Points 93
7.4.1 Syntax 93
7.4.2 Typing 93
7.4.3 Examples 94
8 notes on the implementation 95
8.1 Features of our Implementation 95
8.2 Fixed Points 97
8.2.1 New Syntax for fun 98
8.2.2 Compilation to isstg 99
8.2.3 Read Back 100
8.3 Translation from pts to fun 101
8.3.1 Type Annotations 101
8.3.2 Constructor Saturation 102
8.4 Translation from isstg to x86 Machine Code 103
8.4.1 Memory Model 103
8.4.2 Translation of Instructions 104
8.5 Design Alternatives 106
9 performance evaluation 109
9.1 Benchmark Setting 109
9.2 Peano Numbers 110
9.3 Church 111
6Contents
9.4 Interpretation of the Results 112
10 conclusion 115
10.1 Future Work 115
iv appendix 117
a equivalence of s4 and sstg1 119
a.1 Completeness of Weak Evaluation 119
a.2 of Read Back and Normalization 121
a.3 Soundness of Weak Evaluation 123
a.4 S of Read Back and Normalization 128
b partitioning of sstg2 and isstg reductions 131
b.1 List of Segments 131
c source code of benchmarks 137
c.1 Peano Numbers 137
c.1.1 pts 137
c.1.2 Coq 138
c.1.3 Haskell 139
c.2 Church Numbers 139
c.2.1 pts 139
c.2.2 Coq 140
c.2.3 Haskell 142
7Part I
I N T R O D U C T I O N