Index_C

---

C

C, 6, 45

C^#, 7, see also Java

C++, 6, 226, see also Java

c₀, c₁, c₂, etc. (Church numerals), 60

calculus of constructions, 11, 465

call stack and exception handling, 173–174

call-by-name evaluation, 57

call-by-need evaluation, 57

call-by-value evaluation, 57

call-by-value Y-combinator, 65

call/cc, see continuations

candidate, reducibility, 150

canonical forms lemma, 96, 105, 190, 405, 458

capture-avoiding substitution, 70

cartesian product type, 126–127

casting, 193–196, 247–264, 357, see also ascription

and abstraction, 194

and reflection, 196

as substitute for polymorphism, 195–196

implementation, 196

categorial grammar, 9

category theory, 12

CCS, 34

Cecil, 226, 340

cell, see references

chain, 18

channel types, 200

and subtyping, 200

chapter dependencies, xv

Church encodings

booleans, 58–59

in System F, 347–353

numerals, 60–63

pairs, 60, 396–400

records, 396–400

subtyping, 396–400

Church-Rosser property, 455

Church-style presentation, 111

class, 227, 231

granularity of, 231

classification, type systems as formalisms for, 2

Clean, 338

CLOS, 226, 340

closed set, 282

closed term, 55

closure, 17

property, 289

CLU, 11, 408

codomain of a relation, 16

coercion semantics for subtyping, 200–206, 224

coherence, 204–206

coinduction, 281–313

defined, 282–284

collection classes, 195–196

colored local type inference, 355

combinator, 55

combinatory logic, 76

complete induction, 19

completely bounded quantification, 431

completeness, 212

composition of substitutions, 318

compositionality, 2

comprehension notation for sets, 15

computation rules, 35, 72

computational effects, 153

concrete rule, 27

concrete syntax, 53

confluence, see Church-Rosser property

congruence rules, 35, 72

conservativity of type analyses, 2, 92, 99–100

consistent set, 282

constraint types, 337

constraint-based typing rules, 321–326

constructive logic, 108

constructive type theory, 2, 11

constructors, see type operators

contexts, 76–78

ML implementation, 83–85, 113–115

naming, 77

typing, 101

continuations, 178, 377

contractiveness, 300

contravariant

position in a type, 185

type operator, 473

correctness by construction, 464

countable set, 15

counting subexpressions of μ-types, 304–309

course syllabi, xvii

covariant

position in a type, 185

type operator, 473

cube, Barendregt, 465

Curry-Howard correspondence, 2, 108–109, 341, 429

Curry-style presentation, 111

currying, 58, 73

of type operators, 440

cut elimination, 109

---