Author(s): Stephanie Weirich ICFP’10 Program Chair
Publisher: ACM''
Language: English
Pages: 392
frontmatter.pdf......Page 1
p001-gordon......Page 10
p003-chapman......Page 11
p015-vytiniotis......Page 23
Introduction......Page 35
Replacing the Type of Integers......Page 36
Overview of the Approach......Page 37
Discussion......Page 38
Type System......Page 39
Soundness......Page 40
Alternatives......Page 42
Compiler Implementation......Page 43
Detailed Example......Page 44
Discussions and Conclusions......Page 45
p039-mazurak......Page 47
Introduction......Page 59
The CEK machine......Page 60
The CESK* machine......Page 61
The abstract time-stamped CESK* machine......Page 62
A k-CFA-like abstract CESK* machine......Page 63
Analyzing by-need with Krivine's machine......Page 64
Conditionals, mutation, and control......Page 65
Abstract garbage collection......Page 66
The lambda-sec-calculus and stack-inspection......Page 67
Widening to improve complexity......Page 68
Related work......Page 69
Conclusions and perspective......Page 70
p063-holdermans......Page 71
p075-naylor......Page 83
p087-scott......Page 95
p093-bergstrom......Page 101
p105-bierman......Page 113
Reasoning about Untyped Languages......Page 125
Challenges......Page 126
Propositions and Objects......Page 127
The Base Calculus......Page 128
Typing Rules......Page 129
Pairs......Page 130
The Final Example......Page 131
Operational Semantics......Page 132
From TR to Typed Racket......Page 133
Methodology......Page 134
Related Work......Page 135
Conclusion......Page 136
p129-felleisen......Page 137
p131-crary......Page 139
p143-dreyer......Page 150
p157-reed......Page 163
p169-morgenstern......Page 175
1 Introduction......Page 187
2.1 Syntactic Bidirectionalization......Page 188
2.2 Semantic Bidirectionalization......Page 190
3.1 Specialization to Semantically Linear get-Functions......Page 191
4 Combining Syntactic and Semantic Bidirectionalization......Page 192
5 Analysis of Examples......Page 193
6 Explicit Bias......Page 195
7 Extending Applicability......Page 196
8 Conclusion......Page 197
Acknowledgments......Page 198
Introduction......Page 199
Semantics......Page 201
Matching Lenses......Page 202
Notation......Page 203
Primitives......Page 204
Alignments......Page 206
Nested Chunks......Page 207
Reordering Chunks......Page 208
Conclusions and Future Work......Page 209
p205-hidaka......Page 211
Introduction......Page 223
Working with names and binders......Page 224
The nominal model: logical relations......Page 227
The de Bruijn model: implementation......Page 229
A generic traversal function......Page 230
Applications of the generic traversal......Page 231
Related work......Page 232
Future work......Page 234
p229-crestani......Page 235
p235-culpepper......Page 241
p247-blelloch......Page 253
1 Introduction......Page 254
2.1 Sparse matrix codes in the LL language......Page 255
2.2 Verifying sparse matrix codes......Page 256
3.2 Specification of sparse codes using LL......Page 257
4 Verifying Sparse Codes using Isabelle/HOL......Page 259
4.2 Formalizing vector and matrix representations......Page 260
4.4 Automating the proof......Page 261
5.1 Verifying additional sparse formats......Page 262
5.2 Case study: hierarchical compression formats......Page 263
7 Conclusion......Page 265
p261-keller......Page 266
p273-mccreight......Page 278
p285-danielsson......Page 290
p297-brady......Page 302
p309-mitchell......Page 314
p321-chargueraud......Page 326
p333-stampoulis......Page 338
p345-bernardy......Page 350
Scene i Specification......Page 362
Scene ii Weights......Page 363
Scene i Matching......Page 364
Scene ii Heavy weights......Page 368
Scene iii Experiments......Page 369
Scene ii Laziness......Page 371
Act iv Epilogue......Page 373
p369-pop......Page 374
p375-morris......Page 380
zbackmatter......Page 392
