Types and Programming Languages

identity function, 55

imperative objects, see objects, imperative

implementations

allsome, 381–387

arith, 23–49

bot, 220

equirec, 281–313

fomsub, 467–473

fullequirec, 267–280

fullerror, 171–178

fullfomsub, 389–409, 467–473

fullfsub, 389–409, 417–436

fullfsubref, 411–416

fullisorec, 275–278

fullomega, 439–466

fullpoly, 339–379

fullrecon, 317–338

fullref, 153–170, 225–245

fullsimple, 99–111, 117–146

fullsub, 181–208

fulluntyped, 51–73

fullupdate, 475–489

joinexercise, 223

joinsub, 218–220

purefsub, 417–436

rcdsub, 181–224

recon, 317–338

reconbase, 330

simplebool, 113–116

tyarith, 91–98

untyped, 83–88

implicit type annotations, 330–331

implicitly typed languages, 101

impredicative polymorphism, 340, 360–361

impure language features, 153

induction, 19

lexicographic, 19

logical relations proof technique, 150

mathematical foundations, 282–284

on derivations, 37

on natural numbers, 19

on terms, 29–32

inductive definitions, 23–29

inference, see type reconstruction

inference rules, 26

mathematical foundations, 283

infinite types, 284–286

inheritance, 227

overrated, 245

injection into a sum type, 133

instance of an inference rule, 36

instance variables, 228, 230, 233–234

instanceof, 341

instantiation of a polymorphic function, 317–320, 342

intensional polymorphism, 340

interface, 226

interface types, 479

interfaces (in Java), 261

interference, syntactic control of, 170

intermediate language, 161

intermediate languages, typed, 11

internal language, 53, 120

internet, see web

intersection types, 11, 206–207, 359, 489

and bounded quantification, 400, 409

and normal forms, 206

introduction rule, 108

invariant, 33

inversion lemma

subtyping, 188

typing, 94, 104, 188, 457

iso-recursive types, 275, 280

subtyping, 311–312