Index_S

---

S

safety, 3, 6-8, 95-98

problems with references, 158

problems with references and polymorphism, 335-336

satisfaction of a constraint set by a substitution, 321

saturated sets, 150

Scheme, 2, 6, 8, 45

units, 368

scope, 55

scoping of type variables, 393-394

second-order lambda-calculus, 341, 461

security, type systems and, 9

self, 227, 234-244, 486-488

semantics

alternative styles, 32-34

axiomatic, 33

denotational, 33

operational, 32

semi-unification, 338

semistructured databases, 207

sequences, basic notations, 18

sequencing notation, 119-121

and references, 155

sets, basic operations on, 15

sharing, 445, 465

shifting (of nameless terms), 78-80

ML implementation, 85-87

side effects, 153

simple theory of types, 2

simple types, 100

simplebool implementation, 113-116

simply typed lambda-calculus, 2, 11, 99-111

extensions, 117-146

ML implementation, 113-116

pure, 102

with type operators, 445

Simula, 11, 207

single-field variant, 138-140

singleton kinds, 441, 445, 465

size of a term, 29

small-step operational semantics, 32, 42

Smalltalk, 226

soundness, see safety

soundness and completeness, 212

of algorithmic subtyping, 423

of constraint typing, 325

Source and Sink constructors, 199

spurious subsumption, 253

Standard ML, xvii, 7, 45

statement, 36

static distance, 76

static vs. dynamic typing, 2

store, 153

store typing, 162-165

stratified polymorphism, 360

streams, 270-271

strict vs. non-strict evaluation, 57

String type, 117

strong binary operations, 376

strong normalization, 152, 353

structural operational semantics, 32, 34

structural unfolding, 489

structural vs. nominal type systems, 251-254

stuck term, 41

stupid cast, 259-260

subclass, 227, 232

subexpressions of μ-types, 304-309

subject expansion, 98, 108

subject reduction, see preservation

subscripting conventions, 566

subset semantics of subtyping, 182, 201-202

substitution, 69-72, 75-81, 83-88

capture-avoiding, 70

ML implementation, 85-87

type-, 317

substitution lemma, 106, 168, 189, 453

substitution on types, 342

ML implementation, 382

subsumption, 181-182

postponement of, 214

subtraction of Church numerals, 62

subtype polymorphism, see subtyping

subtyping, 181-224, see also bounded quantification

Top and Bot types, 191-193

algorithm, 209-213, 417-436

algorithmic, in nominal systems, 253

and ascription, 193-196

and base types, 200

and channel types, 200

and objects, 227

and references, 199-200

and type reconstruction, 338, 355

and variant types, 196-197

arrays, 198-199

coercion semantics, 200-206

depth, 183

higher-order, 11, 467-473

intersection types, 206-207

iso-recursive types, 311-312

joins and meets in System F_<:, 432-435

lists, 197

ML implementation, 221-224

objects, 229-230

positive, 489

power types, 472

record permutation, 184

recursive types, 279, 281-290, 298-313

references, 198

reflexivity, 182

subset semantics, 182, 201-202

subtype relation, 182-187

transitivity, 183

type operators, 467-473

undecidability of System F_<:, 427-431

union types, 206-207

vs. other forms of polymorphism, 341

width, 183

sum types, 132-135

super, 234

supertype, 182

support, 290

surface syntax, 53

syllabi for courses, xvii

symmetric relation, 16

syntactic control of interference, 170

syntactic sugar, 121

syntax, 26-29, 52-55, 69

ML implementation, 46-47, 383-385

syntax-directedness, 209

System F, 11, 339-361

fragments, 358-359

history, 341

ML implementation, 381-387

System F_ω, 449-466

and higher-order logic, 109

fragments, 461

System , 467-473

System F_<:, 389-409

kernel and full variants, 391

System λ_ω, 445-447

---