Types and Programming Languages

λNB, 63-66

λ_→, see simply typed lambda-calculus

λ_ω, see System λ_ω

λ_<:, see simply typed lambda-calculus with subtyping

label, 129

lambda cube, 465

lambda-& calculus, 226, 340

lambda-calculi, typed, 2

lambda-calculus, 51, 52

enriched, 63-68

simply typed, see simply typed lambda-calculus

untyped, see untyped lambda-calculus

lambda-term, 53

language definition, defined, 7

language design and type systems, 9-10

language features, pure, 153

late binding, see objects, open recursion

latent type system, 2

lazy evaluation, 57

least fixed point of a generating function, 283

least upper bound, see joins and meets

left-associativity of application, 54

let bindings, 124-125

let-polymorphism, 331-336, 340

exponential behavior, 334

levels, de Bruijn, 81

lexical analysis, 53

lexicographic induction, 19

lexicographic order, 19

LF, 11, 465

lfp algorithm, 294

lightweight formal methods, 1

linear logic and type systems, 11, 109

linking, 367

lists, 146

Church encoding, 350-353, 500

defined using recursive types, 267-270

polymorphic functions for, 345-347

subtyping, 197

local type inference, 355

location, 159

logic

and type systems, 108

origins, 11

type systems in, 2

logical framework, 465

logical relations, 149