| < Free Open Study > |
|
P(S) powerset of S, 15
package, existential, 364
pairs, 126–127
Church encodings, see Church encodings, pairs
parallel reduction, 454
parametric
abbreviation, 439
data type, 142, 444
polymorphism, 319, 340
parametricity, 359–360
parentheses and abstract syntax, 25, 52
parsing, 53
partial evaluation, 109
partial function, 16
partial order, 17
partially abstract types, 406
Pascal, 11
pattern matching, 130–131
PCF, 143
Pebble, 465
Penn translation, 204
Perl, 6
permutation, 18
permutation lemma, 106
permutation rule for record subtyping, 184
performance issues, 201–202
pi-calculus, 51
Pict, 200, 356, 409
Pizza, 195
pointer, 154, see references
arithmetic, 159
pointwise subtyping of type operators, 468
polarity, 473
PolyJ, 195
polymorphic
functions for lists, 345–347
identity function, 342
recursion, 338
update, 482–485
polymorphism, 331
ad hoc, 340
data abstraction, 368–377
existential, see existential types
existential types, 363–379
exponential behavior of ML-style, 334
F-bounded, 393, 408
higher-order, 449–466
impredicativity and predicativity, 360–361
intensional, 340
ML-style, 331–336
parametric, 339–361
parametricity, 359–360
predicative, 360
prenex, 359
rank-2, 359
safety problems with references, 335–336
stratified, 360
subtype, see subtyping
universal, see universal types
varieties of, 340–341
polytype, 359
portability, types and, 7
positive subtyping, 489
Postscript, 6
power types, 445, 472
precedence of operators, 53
predecessor for Church numerals, 62
predicate, 15
predicative polymorphism, 360–361
prenex polymorphism, 359
preorder, 17
preservation of a predicate by a relation, 16
preservation of shapes under type reduction, 456
preservation of types during evaluation, 95–98, 107, 168, 173, 189, 261, 353, 404, 457
preservation of typing under type substitution, 318
principal
type, 317, 329–330
types theorem, 329
typing, 337
unifier, 327
principal solution, 329
principle of safe substitution, 182
product type, 126–127
programming languages
Abel, 409
Algol-60, 11
Algol-68, 11
Amber, 311
C, 6, 45
C#, 7
C++, 6, 226
Cecil, 226, 340
Clean, 338
CLOS, 226, 340
CLU, 11, 408
Dylan, 226
Featherweight Java, 247–264
Forsythe, 11, 199
Fortran, 8, 11
Funnel, 409
FX, 11
GJ, 195, 248, 409
Haskell, 6, 45
Java, 6, 8–10, 45, 119, 137, 154, 174, 177, 178, 193, 195, 196, 198–199, 226, 232, 247–264, 341, 444
KEA, 226
Mercury, 338
ML, 6, 8, 9, 11, 174, 177, see also OCaml, Standard ML
Modula-3, 7
NextGen, 196
Objective Caml, see OCaml
OCaml, xvii, 7, 208, 231, 489
Pascal, 11
Pebble, 465
Perl, 6
Pict, 200, 356, 409
Pizza, 195
PolyJ, 195
Postscript, 6
Quest, 11, 409
Scheme, 2, 6, 8, 45
Simula, 11, 207
Smalltalk, 226
Standard ML, xvii, 7, 45
Titanium, 8
XML, 9, 207, 313
progress theorem, 38, 95–98, 105, 169, 173, 190, 262, 353, 405, 458
projection (from pairs, tuples, records), 126–131
promotion, 418
proof, defined, 20
proof-carrying code, 9
proof theory, 2
proper types, 442
propositions as types, 109
pure λ→, 102
pure lambda-calculus, 51
pure language features, 153
pure type systems, xiv, 2, 444, 466
purefsub implementation, 417–436
| < Free Open Study > |
|