Index_E

---

E

Edinburgh Logical Framework, see LF

effects, 11, 153

efficiency, type systems and, 8

elaboration, 120

elimination rule, 108

encapsulation, 226

encodings, see object encodings

enumerated type, 138

environment, 88

type-, 101

equi-recursive types, 280, 281

equirec implementation, 281-313

equi-recursive types, 275, 281-313

equivalence, see type equivalence

equivalence, behavioral, 64

equivalence relation, 17

erasure, 109-110, 354-358

error, run-time, 42

error detection, use of types for, 4-5

evaluation, 34-43, 72-73

contexts, 261, 262

determinacy of, 37

lazy, 57

ML implementation, 47-49, 87

multi-step, 39

normalization by, 152

of nameless terms, 80-81

strategy, 35

strict vs. non-strict, 57

type-directed partial, 152

untyped lambda-calculus, 55-58

vs. reduction (terminology), 34

exceptions, 171-178

handlers, 171, 174

in Java and ML, 174

subtyping vs. polymorphism in typing of, 192

exercises, difficulty ratings, xviii

existential objects, see objects, existential

existential types, 11, 363-379

and modules, 364

bounded, 406-408

existential unificands, 320

expansion, 98, 108

explicit substitutions, 76, 88

explicitly typed languages, 101

exponential behavior of ML type reconstruction, 334

exposure, type-, 417-418

expressions vs. terms (termionology), 24

extended calculus of constructions, 11

Extended Static Checking, 3

extensible records, see row variables

extensible variant type, 177

extensions of the simply typed lambda-calculus, 117-146

external language, 53, 120

---