Girard J.-Y., Taylor P., Lafont Y. — Proofs and Types :: Электронная библиотека попечительского совета мехмата МГУ

Главная Ex Libris Книги Журналы Статьи Серии Каталог Wanted Загрузка ХудЛит Справка Поиск по индексам Поиск Форум

Авторизация

Поиск по указателям

Girard J.-Y., Taylor P., Lafont Y. — Proofs and Types

Обсудите книгу на научном форуме

Нашли опечатку?
Выделите ее мышкой и нажмите Ctrl+Enter

Название: Proofs and Types

Авторы: Girard J.-Y., Taylor P., Lafont Y.

Аннотация:

Translated (from French) and developed from notes prepared for a course at the University of Paris VII. Deals with the mathematical background of the application to computer science of aspects of logic (namely the correspondence between propositions and types). Treats both the traditional logic material, and its prospective application to computer science.

Язык:

Рубрика: Математика/Алгебра/Математическая логика/

Статус предметного указателя: Готов указатель с номерами страниц

ed2k: ed2k stats

Год издания: 1989

Количество страниц: 176

Добавлена в каталог: 11.12.2004

Операции: Положить на полку | Скопировать ссылку для форума | Скопировать ID

Предметный указатель

(parallel or)      61 70
$\exists$       see “Existential quantifier”
$\lambda$       see “Abstraction”
$\lambda$ -calculus      12 15
$\lambda$ -calculus, Church — Rosser property      22
$\lambda$ -calculus, conversion      18
$\lambda$ -calculus, head normal form      19
$\lambda$ -calculus, natural deduction      11 19
$\lambda$ -calculus, normalisation      24 42
$\lambda$ -calculus, second order polymorphic      82
$\lambda$ -calculus, semantics      54 67
$\lambda$ -calculus, untyped      19 22 133
$\mathcal{L}$ (left logical rules)      see “Sequent calculus”
$\mathcal{P}\omega$       see “Scott”
$\mathcal{R}$ (right logical rules)      see “Sequent calculus”
$\pi$       see “System F”
$\pi^1$ , $\pi^2$ , $\Pi^1$ , $\Pi^2$       see “Components”
$\sum$ (existential type) in F      86 145
$^{\mathcal{L}}$       see “Asymmetrical interpretation”
$^{\mathcal{R}}$       see “Asymmetrical interpretation”
(CR 1—3)      see “Reducibility”
0 (zero)      see “Integers”
Abramsky      i 55
Abstraction $(\lambda)$ conversion      13
Abstraction $(\lambda)$ introduction      12 20
Abstraction $(\lambda)$ realisability      127
Abstraction $(\lambda)$ reducibility      45
Abstraction $(\lambda)$ semantics      68 144
Abstraction $(\lambda)$ syntax      15 82
Absurdity $(\bot)$       6 95
Absurdity $(\bot)$ , commuting conversion      78
Absurdity $(\bot)$ , denotation (f)      see “Booleans and undefined object $(\empty)$ ”
Absurdity $(\bot)$ , empty type (Emp and $\varepsilon_U$ )      80
Absurdity $(\bot)$ , linear logic (\bot and 0)      154
Absurdity $(\bot)$ , natural deduction (\bot\mathcal{E})      73
Absurdity $(\bot)$ , realisability      129
Absurdity $(\bot)$ , sequent calculus (\emptyset\vdash\emptyset)      29
Ackermann’s function      51
Algebraic domain      56
Alive hypothesis      9
All $(\forall)$       see “Universal quantifier”
Alternations of quantifiers      58 124
Alternative conjunction (\&)      see “Direct product”
Amalgamated sum      96 134
Analysis (second order arithmetic)      114
AND      see “Conjunction”
Application, conversion      13
Application, elimination      12 20
Application, realisability      127
Application, reducibility      43
Application, semantics (App)      69
Application, stability (Berry order)      65
Application, syntax      15 82
Application, trace formula (App)      63 64 144
Approximation of points and domains      57 134
Arrow type      see “Implication and function-space”
Associativity of sum type      98
Asymmetrical interpretation      34
Atomic formulae      4 5 30 112 160
Atomic points      see “Tokens”
Atomic sequents      112
Atomic types      15 48
Automated deduction      28 34
Automorphisms      134
Axiom, comprehension      114 118 123
Axiom, excluded middle      6 156
Axiom, hypothesis      10
Axiom, identity      30
Axiom, link      156
Axiom, proper      112
Bad elimination      77
Barendregt      22
Berry      54
Berry order $(\leq _B)$       65 66 135 146
Beta $(\beta)$ rule      see “Conversion”
Binary completeness      56
Binary trees (Bintree)      93
Binding variables      5 12 15 83 161
Boole      3
Booleans      4
Booleans in F $(\Pi X.X\rightarrow X\rightarrow X)$       84 140
Booleans in system F      84
Booleans in T (Bool, T, F)      48 50 70
Booleans, coherence space, $[\Pi X.X\rightarrow X\rightarrow X]$       140
Booleans, coherence space, Bool      56 60 70
Booleans, commuting conversion      86
Booleans, conversion      48
Booleans, denotation (t and f)      4
Booleans, totality      149
Bounded meet      see “Pullback”
Boundedly complete domains      140
Brouwer      6
By values      51 70 91 133
C, C?      see “Contraction”
Camembert      3
CAML      81
Candidate, reducibility      43 115 116
Candidate, totality      58 149
Cantor      1
Cartesian closed category      54 62 67 69 95 152
Cartesian natural transformation      see “Berry order”
Cartesian product      see “Product”
Casewise definition (D)      48 83 97
Category      59 95 133 135
Characteristic subgroup      134
Church — Rosser property      16 22 49 74 79 90 114 152 159
CLIQUE      57 62 101 138
Closed normal form      19 52 121
Coclosure      135
Coherence space      56
Coherence space, $\Pi$ types      143
Coherence space, booleans, $[\Pi X.X\rightarrow X\rightarrow X]$       140
Coherence space, booleans, Bool      56 60 70
Coherence space, coherence relation $( ^\frown_\smile )$       56
Coherence space, direct product (\&)      62
Coherence space, direct sum $(\oplus)$       96 103
Coherence space, empty type $(\mathcal{E}mp)$       104 139
Coherence space, function space (\rightarrow)      64 102 138
Coherence space, integers $[\Pi X.X\rightarrow X\rightarrow X]$       147
Coherence space, integers flat (Int)      56 60 66 70
Coherence space, integers lazy       71 98
Coherence space, linear implication $(\multimap)$       100 104 138
Coherence space, linear negation $(\mathcal{A}^{\bot})$       100 138
Coherence space, of course (!)      101 138 145
Coherence space, Pair, $\Pi^1$ , $\Pi^2$       68
Coherence space, partial functions $(\mathcal{PF})$       66
Coherence space, semantics      67 132
Coherence space, singleton (Sgl)      104 139
Coherence space, tensor product $(\oplus)$       104 138
Coherence space, tensor sum or par $(\maltese)$       104
Coherence space, tokens and web      56
Coherent or spectral space      56
Collect (forming trees)      94
Communicating processes      155
Commutativity of logic      29
Commuting conversion of sum      see “Conversion”
Compact      59 66
Compact-open topology      55
Complementary graph      see “Linear negation”
Complete subgraph      see “Clique”
Complexity, algorithmic      53 111 143
Complexity, logical      42 58 114 122 124 140
Components ( $\pi^1$ and $\pi^2$ ), elimination      19
Components ( $\pi^1$ and $\pi^2$ ), reducibility      43
Composition, stable functions      69
Comprehension scheme      114 118 123 126
Computational significance      1 11 17 112 120
Confluent relation      see “Church — Rosser property”
Conjunction      5
Conjunction and product      11 15 19

Conjunction, conj in Bool      50
Conjunction, conversion      13
Conjunction, cut elimination      105
Conjunction, in F: $\Pi X.(U\rightarrow V\rightarrow X)\rightarrow X      84
Conjunction, linear logic      152
Conjunction, natural deduction, $\wedge\mathcal{I}$ , $\wedge 1\mathcal{E}$ and $\wedge 2\mathcal{E}$       10
Conjunction, realisability      126
Conjunction, sequent calculus, $\mathcal{L}1\wedge$ , $\mathcal{L}2\wedge$ and $\mathcal{R}\wedge$       31
Cons (add to list)      91
Consistency, equational      16 23 152
Consistency, logical (consis)      42 114 124
Constants by vocation      60 66
Constructors      see “Data types in F”
Continuity      54 59 137
Contraction, $\mathcal{LC}$ and $\mathcal{RC}$       29
Contraction, linear logic (C?)      154
Contractum      18 (see also “Redex”
Control features of PROLOG      28
Conversion $(\rightsquigarrow)$       18
Conversion $(\rightsquigarrow)$ in F      83 94
Conversion $(\rightsquigarrow)$ , $\lambda$ -calculus      11 16 18 69
Conversion $(\rightsquigarrow)$ , bogus example      75
Conversion $(\rightsquigarrow)$ , booleans (D)      48
Conversion $(\rightsquigarrow)$ , commuting      74 78 85 97 103
Conversion $(\rightsquigarrow)$ , conjunction $(\wedge)$       13
Conversion $(\rightsquigarrow)$ , degree      25
Conversion $(\rightsquigarrow)$ , denotational equality      69 132
Conversion $(\rightsquigarrow)$ , disjunction $(\vee)$       75 97
Conversion $(\rightsquigarrow)$ , existential quantifier $(\exists)$       75
Conversion $(\rightsquigarrow)$ , implication (\Rightarrow)      13
Conversion $(\rightsquigarrow)$ , infinity (\infty)      72
Conversion $(\rightsquigarrow)$ , integers (R, It)      48 51
Conversion $(\rightsquigarrow)$ , linear logic (proof nets)      158
Conversion $(\rightsquigarrow)$ , natural deduction      13 20
Conversion $(\rightsquigarrow)$ , reducibility      43 116
Conversion $(\rightsquigarrow)$ , rewrite rules      14
Conversion $(\rightsquigarrow)$ , second order      94
Coquand      116 133
Correctness criterion for proof nets      158
Correctness criterion for tokens of IT types      139 142
Couple (forming trees)      93
Cumulative conjunction      see “Tensor product”
Curry — Howard isomorphism      5 150
Curry — Howard isomorphism, conjunction and product      14
Curry — Howard isomorphism, disjunction and sum      80
Curry — Howard isomorphism, implication and functions      14
Curry — Howard isomorphism, none in sequent calculus      28
Curry — Howard isomorphism, second order      94
Cut rule, Cut      30
Cut rule, elimination of      3 105 151 158
Cut rule, linear logic      153 156 158
Cut rule, natural deduction      35 40
Cut rule, not Church — Rosser      150
Cut rule, proofs without      33 159
Cut rule, restriction of      112
D, $\mathcal{D}$       see “Casewise definition”
Data types in F      87 89
Dead hypothesis      9
Deadlock      155
Deduction (natural)      9
Degree $\partial()$ , of formula or type      24 109
Degree d(), of cut or redex      24 109
Delin      see “Linearisation”
Denotation      1
Denotational semantics      14 54 67 95 132
Dereliction (D?)      154
dI-domains      71 98
Direct product (\&), coherence space      61 67
Direct product (\&), linear logic      152
Direct sum $(\oplus)$ , coherence space      96 103 146
Direct sum $(\oplus)$ , coherence space, example      66
Direct sum $(\oplus)$ , linear logic      152
Directed joins      57 59 66
Discharge      9 12 37 73 161
Discrete graph      see “Flat domain”
Disjunction      5 6 95
Disjunction and sum      81
Disjunction, commuting conversion      78
Disjunction, conversion      75
Disjunction, cut elimination      106
Disjunction, disj in Bool      50
Disjunction, intuitionistic $\mathcal{L}\vee$       32
Disjunction, intuitionistic property      8 33
Disjunction, linear logic ( $\oplus$ and $\maltese$ )      152
Disjunction, natural deduction $\vee 1\mathcal{I}$ , $\vee 2\mathcal{I}$ and $\vee\mathcal{E}$       73
Disjunction, sequent calculus $\mathcal{L}\vee$ , $\mathcal{R}1\vee$ and $\mathcal{R}2\vee$       31
Domain theory      56 132
Domain theory, dI-domains      71 98
Domain theory, domain equations      98
Domain theory, Girard versus Scott      54 66 98
Domain theory, L-domains      140
Domain theory, lifted sum      96
Donkey      134
Dynamic      2 14 54
Elimination      8 48
Elimination, $\forall^2\mathcal{E}$       94 125
Elimination, $\vee\mathcal{E}$ , $\bot\mathcal{E}$ and $\exists\mathcal{E}$       73
Elimination, $\wedge 1\mathcal{E}$ , $\wedge 2\mathcal{E}$ , $\Rightarrow\mathcal{E}$ and $\forall\mathcal{E}$       10
Elimination, application and components      19
Elimination, good and bad      77
Elimination, left logical rules      37 40
Elimination, linear logic      161
Elimination, linearity of      99 103
Elimination, R and D in T      48
Embedding-projection pair      133 134
Empty type and absurdity      80
Empty type in F: $Emp = \Pi X. X$       85 139
Empty type, coherence space $(\mathcal{E}mp)$       95 104 139
Empty type, Emp and $\varepsilon_U$       80
Empty type, linear logic ( $\bot$ and 0)      154
Empty type, realisability      129
Equalisers      137
Equations between terms and proofs      see “Conversion”
Espace coherent      56
Eta rule      see “Secondary equations”
Evaluation      see “Application”
Event structures      98
Exchange, $\mathcal{L}X$ and $\mathcal{R}X$       29
Exchange, linear logic (X)      153
Existential quantifier      5 6
Existential quantifier, commuting conversion      78
Existential quantifier, conversion      75
Existential quantifier, cut elimination      108
Existential quantifier, intuitionistic property      8 33
Existential quantifier, natural deduction, $\exists\mathcal{I}$ and $\exists\mathcal{E}$       73
Existential quantifier, sequent calculus, $\mathcal{L}\exists$ and $\mathcal{R}\exists$       32
Existential type in F $(\sum,\nabla)$       86 145
Exponential object      see “Implication and function-space”
Exponential process      see “Complexity algorithmic”
Expressive power      50 89 155
Extraction      see “Universal application”
F (Girard — Reynolds system), representable functions      120
F (Girard — Reynolds system), semantics      132
F (Girard — Reynolds system), strong normalisation      42 114
F (Girard — Reynolds system), syntax      82
False denotation $(f,\mathcal{F},F)      see “Booleans”
False proposition $(\bot)$       see “Absurdity”
feasible      see “Complexity algorithmic”
Fields of numbers      134
Filtered colimits      59 137
Finite approximation      57 66 132 134
Finite branching tree      27
Finite normalisation      24
Finite points $(\mathcal{A}_{fin})$       57
Finite presentability      66
Finite, sense and denotation      2
Finite, very      59 66
Fixed point      72 95
Flat domain      57 60 66 70 140
For all $(\forall)$       see “Universal quantifier”

1 2 3

О проекте