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

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

Reflexive symmetric relation      57
Representable functions      52 120
Resolution method      112
Rewrite rules      see “Conversion”
Reynolds      82
Right logical rules      see “Sequent calculus”
Rigid embeddings      134
Ring theory      66
Robinson      112
rosser      see “Church — Rosser property”
S, S (successor)      see “Integers”
Saturated domains      133
Scott      54 55 64 66 133
Second incompleteness theorem      42
Second order logic      94 114 123
Secondary equations      16 69 81 85 97 132
Semantic definability      140
Sense      1
Separability      134
Sequent calculus      28
Sequent calculus, Cut rule      30
Sequent calculus, linear logic      150
Sequent calculus, logical rules      31
Sequent calculus, natural deduction      35
Sequent calculus, PROLOG      112
Sequent calculus, structural rules      29
Sequential algorithm      54
Side effects      150
Signature      34 87 139
Simple types      84 139 145
Singleton type (Sgl)      104 139
Size problem      83 112 132
Smyth      55
SN (strongly normalisable terms)      119
Specification      17
Spectral space      56
Stability      54 134 137
Stability, definition (St)      58 100
static      2 14 54
Strict (preserve $\emptyset$ )      97
Strong finiteness      59 66
Strong normalisation      26 42 114
Structural rules, cut elimination      106 112
Structural rules, linear logic      152 153
Structural rules, natural deduction      36
Structural rules, sequent calculus      29
Subdomain      134
Subformula property, $\lambda$ -calculus      19
Subformula property, natural deduction      76
Subformula property, sequent calculus      33
Substantifique moelle      155
Substitution      5 25 69 112 118
Subuniformity      134
Successor (S and S)      see “Integers”
Sum type      95
Sum type and disjunction      81
Sum type, +, $\iota^1$ , $\iota^2$ and $\delta$       81
Sum type, coherence space      103 146
Sum type, linear decomposition      96 103
Sum type, linear logic ( $\oplus$ and $\maltese$ )      152
Symmetry      10 18 28 30 31 97 105 134
T (Godel’s system)      47 67 70 123
T, t, $\mathcal{T}$       see “True”
Tableaux      28

Tait      42 49 114
Takeuti      125
Tarski      4
Tautology, linear logic (1 and $\top$ )      154
Taylor      133
Tensor product $(\otimes)$ , coherence space      104 138 146
Tensor product $(\otimes)$ , linear logic      152
Tensor sum or par $(\maltese)$ , coherence space      104
Tensor sum or par $(\maltese)$ , linear logic      152
Terminal object      104
Terminating relation      see “Normalisation”
Terms in       125
Terms in F      82
Terms in T      68
Terms, $\lambda$ -calculus      15
Terms, object language      5
Theory of constructions      116 133
Token      56 64 137
Topological space      55
Total category      135 137 141 146
Total objects      57 149
Total recursive function      53 122
Trace (Tr)      62 67 144
Trace, linear (Trlin)      100
Transposition in linear algebra      101
Trees      8 47 93
True, denotation (t, $\mathcal{T}$ , T)      see “Booleans”
True, proposition $(\top)$       see “Tautology”
Turbo cut elimination      160
Turing      122
Type variables      82
Types      15 54 67
Undefined object $(\empty)$       56 96 129 139 146 149
Unification      113
Uniform continuity      55
Uniformity of $\Pi$ types      83 132 134 143
Units (0, $\top$ , 1 and $\bot$ )      104
Universal algebra      66
Universal domain      133
Universal program (Turing)      122
Universal quantifier      5 6
Universal quantifier (second order)      82 126
Universal quantifier (second order), $\forall^2\mathcal{I}$ and $\forall^2\mathcal{E}$       94 125
Universal quantifier (second order), reducibility      118
Universal quantifier (second order), semantics      132 143 149
Universal quantifier, cut elimination      108
Universal quantifier, natural deduction, $\forall\mathcal{I}$ and $\forall\mathcal{E}$       10
Universal quantifier, sequent calculus, $\mathcal{L}\forall$ and $\mathcal{R}\forall$       32
Variable coherence spaces      141
Variables, hypotheses      11 15 19
Variables, object language      10 125
Variables, type      82 125
Very finite      59 66
Vickers      55
Weak normalisation      24
Weakening, $\mathcal{L} W$ and $\mathcal{R} W$       29
Weakening, linear logic (W?)      154
Web      56 135
Why not (?)      102 154
Winskel      98 133
X, $\mathcal{L}X$ , $\mathcal{R}X$ (exchange)      29 153
Y (fixed point)      72
Zero, 0, unit of $\oplus$       154
Zero, O and $\mathcal{O}$       see “Integers”

1 2 3

О проекте