| < Free Open Study > |
|
ramified theory of types, 2
range of a relation, 16
rank-2 polymorphism, 359
raw type, 248
rcdsub implementation, 181–224
reachableF, 294
recon implementation, 317–338
reconbase implementation, 330
reconstruction, see type reconstruction
record kinds, 445
records, 129–131
Cardelli-Mitchell calculus, 207
Church encoding, 396–400
concatenation, 207
row variables, 208, 337
recursion, 65–66, 142–145
fixed-point combinator, 65
polymorphic, 338
recursive types, 253, 267–280
Amadio-Cardelli algorithm, 309–311
and subtyping, 279
equi-recursive vs. iso-recursive, 275
history, 279–280
in ML, 277–278
in nominal systems, 253
metatheory, 281–313
μ notation, 299–304
subtyping, 281–290, 298–313
type reconstruction, 313, 338
recursive values from recursive types, 273
redex, 56
reduce function, 63
reducibility candidates, 150
reduction vs. evaluation (terminology), 34
references, 153–170
allocation, 154
and subtyping, 199–200
assignment, 154
dereferencing, 154
subtyping, 198
type safety problems, 158
type safety problems with polymorphism, 335–336
refinement types, 207
reflection, 196, 252
and casting, 196
reflexive closure, 17
reflexive relation, 16
reflexivity of subtyping, 182
region inference, 8
regular trees, 298–299
relation, 15
logical, see logical relations
removenames, 78
representation independence, 371
representation of numbers by Church numerals, 67
representation type (of an object), 230
restorenames, 78
row kinds, 445
row variables, 11, 208, 337, 489
rule
computation, 35, 72
congruence, 35, 72
naming conventions, 565
schema, 27
rule, inference, 27
rule schema, 27
rules
B-IFFALSE, 43
B-IFTRUE, 43
B-ISZEROSUCC, 43
B-ISZEROZERO, 43
B-PREDSUCC, 43
B-PREDZERO, 43
B-SUCC, 43
B-VALUE, 43
CT-ABS, 322, 542
CT-ABSINF, 330
CT-APP, 322, 542
CT-FALSE, 322
CT-FIX, 543
CT-IF, 322
CT-ISZERO, 322
CT-LETPOLY, 332
CT-PRED, 322
CT-PROJ, 545
CT-SUCC, 322
CT-TRUE, 322
CT-VAR, 322, 542
CT-ZERO, 322
E-ABS, 502
E-APP1, 72, 103, 160, 166, 186, 343, 392, 446, 450, 470, 502, 503
E-APP2, 72, 103, 160, 166, 186, 343, 392, 446, 450, 470, 502
E-APPABS, 72, 81, 103, 160, 166, 186, 342, 343, 392, 446, 450, 470, 502, 503
E-APPERR1, 172
E-APPERR2, 172
E-APPRAISE1, 175
E-APPRAISE2, 175
E-ASCRIBE, 122, 194
E-ASCRIBE1, 122
E-ASCRIBEEAGER, 123
E-ASSIGN, 161, 166
E-ASSIGN1, 161, 166
E-ASSIGN2, 161, 166
E-CASE, 132, 136
E-CASEINL, 132, 135
E-CASEINR, 132, 135
E-CASEVARIANT, 136
E-CAST, 258
E-CASTNEW, 258
E-CONS1, 147
E-CONS2, 147
E-DEREF, 161, 166
E-DEREFLOC, 161, 166
E-DOWNCAST, 195
E-FIELD, 258
E-FIX, 144
E-FIXBETA, 144
E-FLD, 276
E-FUNNY1, 40
E-FUNNY2, 40
E-GC, 514
E-HEAD, 147
E-HEADCONS, 147
E-IF, 34
E-IF-WRONG, 42
E-IFFALSE, 34
E-IFTRUE, 34
E-INL, 132, 135
E-INR, 132, 135
E-INVK-ARG, 258
E-INVK-RECV, 258
E-INVKNEW, 258
E-ISNIL, 147
E-ISNILCONS, 147
E-ISNILNIL, 147
E-ISZERO, 41
E-ISZERO-WRONG, 42
E-ISZEROSUCC, 41
E-ISZEROZERO, 41
E-LET, 124, 131, 335
E-LETV, 124, 131, 332
E-NEW-ARG, 258
E-PACK, 366, 452
E-PAIR1, 126
E-PAIR2, 126
E-PAIRBETA1, 126
E-PAIRBETA2, 126
E-PRED, 41
E-PRED-WRONG, 42
E-PREDSUCC, 41, 48
E-PREDZERO, 41
E-PROJ, 128, 129, 187
E-PROJ1, 126
E-PROJ2, 126
E-PROJNEW, 258
E-PROJRCD, 129, 187, 201, 484
E-PROJTUPLE, 128
E-RAISE, 175
E-RAISERAISE, 175
E-RCD, 129, 187, 484
E-REF, 162, 166
E-REFV, 162, 166
E-SEQ, 120
E-SEQNEXT, 120
E-SUCC, 41
E-SUCC-WRONG, 42
E-TAIL, 147
E-TAILCONS, 147
E-TAPP, 343, 392, 450, 470
E-TAPPTABS, 342, 343, 385, 392, 450, 470
E-TRY, 174, 175
E-TRYERROR, 174
E-TRYRAISE, 175
E-TRYV, 174, 175
E-TUPLE, 128
E-TYPETEST1, 195
E-TYPETEST2, 195
E-UNFLD, 276
E-UNFLDFLD, 276
E-UNPACK, 366
E-UNPACKPACK, 366, 367, 452
E-UPDATEV, 484
E-VARIANT, 136
E-WILDCARD, 507
K-ABS, 446, 450, 470
K-ALL, 450, 470
K-APP, 446, 450, 470
K-ARROW, 446, 450, 470
K-SOME, 452
K-TOP, 470
K-TVAR, 446, 450, 470
M-RCD, 131
M-VAR, 131
P-RCD, 509
P-RCD', 509
P-VAR, 509
Q-ABS, 446, 451, 471
Q-ALL, 451, 471
Q-APP, 446, 451, 471
Q-APPABS, 441, 446, 451, 471
Q-ARROW, 446, 451, 471
Q-REFL, 446, 451, 471
Q-SOME, 452
Q-SYMM, 446, 451, 471
Q-TRANS, 446, 451, 471
QR-ABS, 454
QR-ALL, 454
QR-APP, 454
QR-APPABS, 454
QR-ARROW, 454
QR-REFL, 454
S-ABS, 468, 471
S-ALL, 392, 394, 395, 427, 471
S-AMBER, 311
S-APP, 468, 471
S-ARRAY, 198
S-ARRAYJAVA, 198
S-ARROW, 184, 186, 211, 392, 471
S-ASSUMPTION, 311
S-BOT, 192
S-EQ, 468, 471
S-INTER1, 206
S-INTER2, 206
S-INTER3, 206
S-INTER4, 206
S-LIST, 197
S-PRODDEPTH, 187
S-PRODWIDTH, 187
S-RCD, 211
S-RCDDEPTH, 183, 187, 484
S-RCDPERM, 184, 187
S-RCDVARIANCE, 484
S-RCDWIDTH, 183, 187, 484
S-REF, 198
S-REFL, 182, 186, 211, 392
S-REFSINK, 199
S-REFSOURCE, 199
S-SINK, 199
S-SOME, 406, 476, 556
S-SOURCE, 199
S-TOP, 185, 186, 211, 392, 471
S-TRANS, 183, 186, 209, 211, 392, 471
S-TVAR, 392, 394, 471
S-VARIANTDEPTH, 197
S-VARIANTPERM, 197
S-VARIANTWIDTH, 197
SA-ALL, 422, 424
SA-ARROW, 212, 422, 424
SA-BOT, 220
SA-RCD, 212
SA-REFL-TVAR, 422, 424
SA-TOP, 212, 422, 424
SA-TRANS-TVAR, 422, 424
T-ABS, 101, 103, 167, 186, 343, 392, 447, 451, 471
T-APP, 102, 103, 167, 181, 186, 343, 392, 447, 451, 471
T-ASCRIBE, 122, 194
T-ASSIGN, 159, 165, 167, 199
T-CASE, 132, 136
T-CAST, 530
T-CONS, 147
T-DCAST, 259
T-DEREF, 159, 165, 167, 199
T-DOWNCAST, 194
T-EQ, 441, 447, 451
T-ERROR, 172
T-EXN, 175
T-FALSE, 93
T-FIELD, 259
T-FIX, 144
T-FLD, 276
T-HEAD, 147
T-IF, 93, 102, 218
T-INL, 132, 135
T-INR, 132, 135
T-INVK, 259
T-ISNIL, 147
T-ISZERO, 93
T-LET, 124, 332, 509
T-LETPOLY, 332, 333
T-LOC, 164, 167
T-NEW, 259
T-NIL, 147
T-PACK, 365, 366, 406, 452
T-PAIR, 126
T-PRED, 93
T-PROJ, 128, 129, 187, 484
T-PROJ1, 126
T-PROJ2, 126
T-RCD, 129, 187, 484
T-REF, 159, 165, 167
T-SCAST, 259
T-SEQ, 120
T-SUB, 182, 186, 209, 392, 471
T-SUCC, 93
T-TABS, 342, 343, 392, 395, 451, 471
T-TAIL, 147
T-TAPP, 342, 343, 392, 395, 451, 471
T-TRUE, 93
T-TRY, 174, 175
T-TUPLE, 128
T-TYPETEST, 195
T-UCAST, 259
T-UNFLD, 276
T-UNIT, 119, 167
T-UNPACK, 366, 406, 435, 452
T-UPDATE, 484
T-VAR, 101, 103, 167, 186, 259, 343, 392, 447, 451, 471
T-VARIANT, 136, 197
T-WILDCARD, 507
T-ZERO, 93
TA-ABS, 217, 419
TA-APP, 217, 419
TA-APPBOT, 220
TA-IF, 220, 526
TA-PROJ, 217
TA-PROJBOT, 220
TA-RCD, 217
TA-TABS, 419
TA-TAPP, 419
TA-UNPACK, 436
TA-VAR, 217, 419
XA-OTHER, 418
XA-PROMOTE, 418
run-time code generation, 109
run-time error, 42
trapped vs. untrapped, 7
run-time monitoring, 1
| < Free Open Study > |
|