Bertot Y., Castéran P. — Interactive Theorem Proving and Program Development: Coq'ArtiThe Calculus of Inductive Constructions :: Электронная библиотека попечительского совета мехмата МГУ

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

Авторизация

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

Bertot Y., Castéran P. — Interactive Theorem Proving and Program Development: Coq'ArtiThe Calculus of Inductive Constructions

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

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

Название: Interactive Theorem Proving and Program Development: Coq'ArtiThe Calculus of Inductive Constructions

Авторы: Bertot Y., Castéran P.

Аннотация:

Coq is an interactive proof assistant for the development of mathematical theories and formally certified software. It is based on a theory called the calculus of inductive constructions, a variant of type theory.
This book provides a pragmatic introduction to the development of proofs and certified programs using Coq. With its large collection of examples and exercises it is an invaluable tool for researchers,students, and engineers interested in formal methods and the development of zero-fault software.

Язык:

Рубрика: Математика/

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

ed2k: ed2k stats

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

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

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

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

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

Theorems, S_to_plus_one      207
Theorems, then_example      62
Theorems, then_fail_example      64
Theorems, then_fail_example2      64
Theorems, triple_impl      61
Theorems, triple_impl2      70
Theorems, triple_impl_one_shot      62
Theorems, TrivialDict.diff_key      341
Theorems, TrivialDict.empty_def      341
Theorems, TrivialDict.success      341
Theorems, try_example      64
Theorems, unfold_example      116
Theorems, Vconseq      223
Theorems, vect_to_list_and_back      223
Theorems, xy_ord      215
Theorems, zero_cons_ord      215
Theorems, Zle_Pfact      236
Theorems, Zmult_distr_l      126
Type definitions, Co-inductive, Always      374
Type definitions, Co-inductive, bisimilar      368
Type definitions, Co-inductive, Infinite      363
Type definitions, Co-inductive, LList      349
Type definitions, Co-inductive, Stream      348
Type definitions, Co-inductive, Trace      375
Type definitions, Inductive, Acc      293 398
Type definitions, Inductive, and      219
Type definitions, Inductive, Atomic      372
Type definitions, Inductive, automaton      375
Type definitions, Inductive, bin      439
Type definitions, Inductive, bool      17 137
Type definitions, Inductive, btree      343
Type definitions, Inductive, clos_trans      212
Type definitions, Inductive, direction      351
Type definitions, Inductive, div_data      281
Type definitions, Inductive, Empty_set      184
Type definitions, Inductive, eq      220 396
Type definitions, Inductive, even      212 246
Type definitions, Inductive, Eventually      373
Type definitions, Inductive, even_line      185
Type definitions, Inductive, ex      219
Type definitions, Inductive, exec      240
Type definitions, Inductive, False      218
Type definitions, Inductive, Finite      361
Type definitions, Inductive, htree      288
Type definitions, Inductive, INSERT      314 343
Type definitions, Inductive, inst      239
Type definitions, Inductive, is_0_1      244
Type definitions, Inductive, JMeq      220
Type definitions, Inductive, le      212
Type definitions, Inductive, list      377
Type definitions, Inductive, log2_domain      429
Type definitions, Inductive, log_domain      428
Type definitions, Inductive, ltree      181 404
Type definitions, Inductive, maj      312
Type definitions, Inductive, min      312
Type definitions, Inductive, month      138
Type definitions, Inductive, Next      373
Type definitions, Inductive, nforest      400
Type definitions, Inductive, ntree      400
Type definitions, Inductive, occ      310
Type definitions, Inductive, occurs      401
Type definitions, Inductive, occurs_forest      401
Type definitions, Inductive, option      177
Type definitions, Inductive, or      219
Type definitions, Inductive, Pfact      234
Type definitions, Inductive, plane      145
Type definitions, Inductive, positive      167 287
Type definitions, Inductive, prod      179
Type definitions, Inductive, RM      314
Type definitions, Inductive, RMAX      322
Type definitions, Inductive, Rpos_div2      412
Type definitions, Inductive, search_tree      312
Type definitions, Inductive, sig      252
Type definitions, Inductive, sigS      254

Type definitions, Inductive, sorted      212
Type definitions, Inductive, south_west      212
Type definitions, Inductive, sqrt_data      181
Type definitions, Inductive, strange      184
Type definitions, Inductive, sum      180
Type definitions, Inductive, sumbool      254
Type definitions, Inductive, True      218
Type definitions, Inductive, vehicle      147
Type definitions, Inductive, Z      167
Type definitions, Inductive, Z_btree      167 309
Type definitions, Inductive, Z_fbtree      170
Type definitions, Inductive, Z_inf_branch_tree      171
Type definitions, Plain definitions, lt      105
Type definitions, Plain definitions, not      99
Type definitions, Plain definitions, relation      212
Type definitions, Plain definitions, Zwf      236
Type definitions, Theorems, Co-inductive, LTree      349
Typing rules, App      21 75 81
Typing rules, App*      22
Typing rules, Conv      40
Typing rules, Lam      25 84
Typing rules, Let-in      27
Typing rules, Prod      52 76 78 91
Typing rules, Prod-Prop      51
Typing rules, Prod-Set      38
Typing rules, Var      21 52
Vernacular, Abort      57
Vernacular, Add Ring      196
Vernacular, Add Semi Ring      196
Vernacular, Axiom      46
Vernacular, Check      15 51
Vernacular, CoFixpoint      352
Vernacular, CoInductive      348
Vernacular, Declare Module      328
Vernacular, Defined      115 410 429
Vernacular, Definition      29
Vernacular, Eval      33
Vernacular, Fixpoint      164 385
Vernacular, Hint      191
Vernacular, Hint, Resolve      191 215
Vernacular, Hint, Rewrite      194 360
Vernacular, Hypotheses      46
Vernacular, Hypothesis      46
Vernacular, Implicit Arguments      88
Vernacular, Lemma      48
Vernacular, Let      33
Vernacular, Locate      14 278
Vernacular, Module Type      327
Vernacular, Opaque      59
Vernacular, Open Scope      14
Vernacular, Parameter      29
Vernacular, Print      29 89
Vernacular, Print Scope      15
Vernacular, Proof      47 53
Vernacular, Qed      50 53 115
Vernacular, Record      146
Vernacular, Require      13
Vernacular, Reset      19
Vernacular, Reset, Initial      19
Vernacular, Restart      57
Vernacular, Save      58
Vernacular, Scheme      394 401 430
Vernacular, SearchPattern      114 203 237 278 403
Vernacular, SearchRewrite      129 203 280
Vernacular, Set Implicit Arguments      89
Vernacular, Set Printing Notations      23
Vernacular, Show      57
Vernacular, Theorem      47
Vernacular, Transparent      59
Vernacular, Undo      365
Vernacular, Unset Implicit Arguments      89
Vernacular, Unset Printing Notations      23
Vernacular, Variable      31
Vernacular, Variables      31

1 2 3

О проекте