Index

Alberto Carraro, 1
Alessi, Fabio, 2
Antonino Salibra, 3

Barendregt, Henk, 4, 5, 6, 7
Barendregt-Geuvers-Klop conjecture, 8
Basis Decision Problem, 9
Berline,Chantal, 10
Böhm tree, 11

category, 12
    bicartesian closed, 13
    cartesian closed, 14
combinator
     $ω$ , 15
     $B$ , 16, 17
     $B ′$ , 18
     $I$ , 19
     $W$ , 20
     $Y$ , 21
    ﬁxed-point, 22
    Lark, 23
    proper, 24
combinatory logic, 25, 26, 27, 28, 29
conﬂuence, 30, 31
congruence, 32
contextual equivalence, 33
coproduct, 34
Curry, Haskell, 35

David, René, 36
Dezani-Ciancaglini, Mariangiola, 37, 38, 39, 40, 41

easiness, 42

Geuvers, Herman, 43, 44
Giannini, Paola, 45

Henglein, Fritz, 46
hereditary permutation, 47
Hindley, Roger, 48, 49
Honsell, Furio, 50, 51

inductive types, 52
inhabitation problem, 53
intersection types, 54, 55, 56

K-conjecture, 57
Klop, Jan Willem, 58

lambda-theory, 59, 60, 61

matching, 62
Meyer, Robert, 63
Minari, Pierluigi, 64

normalization, 65, 66

order
of a combinator, 67
of a constructor, 68

Plotkin terms, 69
polymorphism, 70
Pottier, François, 71
PTS, 72
pure type system, 73

range problem
for $ℋ$ , 74
recursive types, 75, 76, 77, 78
reduction strategy, 79
Rehof, Jakob, 80
retraction, 81
Ronchi Della Rocca, Simona, 82

Severi, Paula, 83, 84
Simpson, Alex, 85
Smith, Scott, 86
Smullyan, Raymond, 87
Spławski, Zdzisław, 88
Statman, Richard, 89, 90, 91, 92, 93, 94, 95, 96, 97
strong reduction, 98
substructural logic, 99
subtype entailment, 100
system
$F$ , 101
$Fω$ , 102, 103, 104
Sørensen, Morten Heine, 105

Tatsuta, Makoto, 106
term
easy, 107
theory
$ℋ$ , 108
ticket entailment, 109, 110
Trifonov, Valery, 111
typability, 112, 113, 114
type system, 115

universal generator, 116
Urzyczyn, Paweł, 117, 118, 119, 120, 121, 122

de Vries, Fer-Jan, 123

word problem, 124, 125