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

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

blank
blank
blank
Красота
blank
Bertot Y., Castéran P. — Interactive Theorem Proving and Program Development: Coq'ArtiThe Calculus of Inductive Constructions
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.


Язык: en

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

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

ed2k: ed2k stats

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

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

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

Операции: Положить на полку | Скопировать ссылку для форума | Скопировать ID
blank
Предметный указатель
Plain definitions, eq_dec      255
Plain definitions, example_codomain      387
Plain definitions, excluded_middle      123
Plain definitions, F_Infinite      374
Plain definitions, G_Infinite      374
Plain definitions, implies_to_or      123
Plain definitions, insert_spec      314 343
Plain definitions, isEmpty      351
Plain definitions, is_prime      205
Plain definitions, leibniz      131
Plain definitions, Lexico.A      338
Plain definitions, Lexico.le      338
Plain definitions, list2tree_spec      319
Plain definitions, LKey.A      333
Plain definitions, long      76
Plain definitions, More_Dec_Orders.A      336
Plain definitions, More_Dec_Orders.le      336
Plain definitions, More_Dec_Orders.lt      336
Plain definitions, my_and      133
Plain definitions, my_ex      133
Plain definitions, my_False      130
Plain definitions, my_le      134
Plain definitions, my_not      131
Plain definitions, my_or      133
Plain definitions, my_True      130
Plain definitions, Nats.data      342
Plain definitions, nat_fun_to_Z_fun      41
Plain definitions, Nat_Order.A      338
Plain definitions, Nat_Order.le      338
Plain definitions, Nat_Order.lt      338
Plain definitions, neutral_left      107
Plain definitions, occ_dec      315
Plain definitions, occ_dec_spec      313 343
Plain definitions, PairKey.A      333
Plain definitions, peirce      123
Plain definitions, rich_minus      395
Plain definitions, rmax_sig      322
Plain definitions, rmax_spec      322
Plain definitions, rm_spec      314
Plain definitions, satisfies      372
Plain definitions, short      76
Plain definitions, stronger_prime_test      264
Plain definitions, TDict.data      343
Plain definitions, TDict.dict      344
Plain definitions, TDict.key      343
Plain definitions, TrivialDict.data      341
Plain definitions, TrivialDict.dict      341
Plain definitions, TrivialDict.key      341
Plain definitions, ZKey.A      329
Plain definitions, Z_bin      40
Syntax, cofix      352
Syntax, fix      190 284
Syntax, let in      27
Syntax, match      142 145
Tacticals, orelse      63
Tacticals, repeat      123
Tacticals, try      64
Tactics, apply      48 53 108 139 141
Tactics, apply, apply with      110
Tactics, assert      68
Tactics, assoc_eq      444
Tactics, assoc_eq_nat      441
Tactics, assumption      49 52 105
Tactics, auto      139 149 200 215
Tactics, auto, with      190
Tactics, autoAfter      202
Tactics, autoClear      202
Tactics, autorewrite      194 360 362
Tactics, case      160 188
Tactics, caseEq      160
Tactics, cbv      36 189 435
Tactics, change      152 154 188
Tactics, check_It_not_divides      205
Tactics, check_not_divides      203
Tactics, clear      70 193 202 284
Tactics, clear_all      206
Tactics, cofix      364
Tactics, comm_eq      447
Tactics, compute      36 278
Tactics, compute_rank      444
Tactics, constructor      227
Tactics, contrapose      204
Tactics, cut      68 242
Tactics, dependent rewrite      221
Tactics, destruct      188
Tactics, discriminate      151
Tactics, div_bin_tac      280
Tactics, eapply      111 194 243
Tactics, eauto      194 242 243
Tactics, eexact      112 194
Tactics, elim      118 121 141 160 217 241 244
Tactics, elim, using      270 430
Tactics, elim, with      141
Tactics, exact      52 105
Tactics, exists      123 227
Tactics, fail      64
Tactics, field      199
Tactics, fold      190 280
Tactics, fourier      200
Tactics, generalize      157 248 275
Tactics, idtac      64
Tactics, induction      142 187 227 229
Tactics, injection      153 249
Tactics, intro      106 139
Tactics, intros      48 225
Tactics, intuition      122 201
Tactics, inversion      247
Tactics, lazy      189 280 435
Tactics, left      219 227
Tactics, le_S_star      202
Tactics, LList_unfold      360
Tactics, model      441
Tactics, model_A      444
Tactics, model_aux      444
Tactics, omega      198 260
Tactics, pattern      127 139 159 160 245 248
Tactics, refine      265 282 315
Tactics, reflexivity      124
Tactics, rewrite      125 207 220 225
Tactics, rewrite in      126
Tactics, rewrite, rewrite <-      126
Tactics, right      219 227
Tactics, ring      125 196
Tactics, ring_nat      198 417
Tactics, simpl      144 188 267 435
Tactics, simpl at $arg$      189
Tactics, simpl_on      210
Tactics, split      227
Tactics, subst      195
Tactics, S_to_plus_simpl      207
Tactics, tauto      122 200
Tactics, term_list      444
Tactics, trivial      71
Tactics, unfold      115
Theorems, absurd      119
Theorems, all_imp_dist      110
Theorems, all_perm      97
Theorems, and_commutes      121
Theorems, any_height_inj2      221
Theorems, apply_example      54
Theorems, at_least_28      148
Theorems, bad_get_primediv_ok      263
Theorems, bdiv_aux_correctl      408
Theorems, bicycle_eq_seats      153
Theorems, compose_example      63
Theorems, cond_rewrite_example      128
Theorems, conj3      100
Theorems, conj3’      121
Theorems, contrap      120
Theorems, conv_example      105
Theorems, cut_example      69
Theorems, delta      53
Theorems, diff_of_squares      125
Theorems, disj4_3      100
Theorems, disj4_3’      121
Theorems, div      it_correct 1 426
Theorems, div2_le      267 268
Theorems, divides_refl      262
Theorems, div_bin_eq      281
Theorems, div_bin_rem_lt      280
Theorems, div_it_fix_eqn      425
Theorems, double_neg_i      119
Theorems, double_neg_i’      120
Theorems, elim_example      245
Theorems, eq_sym’      125
Theorems, eq_trans      129
Theorems, Eventually_of_LAppend      373
Theorems, example_contrapose      204
Theorems, example_for_field      199
Theorems, example_for_Fourier      200
Theorems, example_for_subst      195
Theorems, example_intuition      201
Theorems, ex_imp_ex      123
Theorems, fact_def_pos      235
Theorems, Finite_of_LCons      362
Theorems, flatten_aux_valid      440
Theorems, flatten_aux_valid_A      443
Theorems, flatten_valid      440
Theorems, flatten_valid_2      440
Theorems, flatten_valid_A      443
Theorems, flatten_valid_A_2      443
Theorems, from_Infinite      364
Theorems, from_Infinite_V0      364
Theorems, get_primediv_ok      264
Theorems, greater_values_sum      402
Theorems, HoareWhileRule      240
Theorems, imp_dist      54 65
Theorems, imp_trans      47 51 107
Theorems, inject_c2      155
Theorems, insert_is_f      446
Theorems, K      56
Theorems, keep_length      223
Theorems, LAppend_assoc      370
Theorems, LAppend_LCons      357 360
Theorems, LAppend_LNil      360
Theorems, LAppend_of_Finite      362
Theorems, lazy_example      190
Theorems, leibniz_sym      132
Theorems, length_february      144
Theorems, le_0_mult      113
Theorems, le_0_mult_R      113
Theorems, le_2_n_not_zero      259
Theorems, le_2_n_pred      259
Theorems, le_2_n_pred’      259
Theorems, le_5_25      202
Theorems, le_i_SSi      86 109
Theorems, le_mult_mult      110
Theorems, le_mult_mult’      111
Theorems, le_plus_minus’      188
Theorems, LList_decomposition_lemma      358
Theorems, LNil_not_Infinite      367
Theorems, log2_domain_invert      429
Theorems, log_domain_non_0      428
Theorems, lt_Acc      412
Theorems, lt_le      229
Theorems, lt_S      115
Theorems, lt_wf      412
Theorems, max 1_correct      425
Theorems, max2_correct      425
Theorems, modus_ponens      120
Theorems, month_equal      139
Theorems, More_Dec_Orders .le_trans      336
Theorems, More_Dec_Orders. It_ir reflexive      336
Theorems, More_Dec_Orders.lt_intro      336
Theorems, my_False_ind      131
Theorems, my_I      131
Theorems, nat_2_ind      270
Theorems, nat_not_strange      185
Theorems, Nat_Order.It_diff      338
Theorems, Nat_Order.le_lt_or_eq      338
Theorems, Nat_Order.le_lt_weak      338
Theorems, Nat_Order.ordered      338
Theorems, next_august_then_july      151
Theorems, Next_example      373
Theorems, next_march_shorter      157
Theorems, not_decreasing      415
Theorems, not_even_l      248
Theorems, not_January_eq_February      152
Theorems, not_l_even      246
Theorems, not_l_even’      247
Theorems, obtain_I      194
Theorems, omega_example1      198
Theorems, omega_example2      198
Theorems, omega_example3      199
Theorems, omega_example4      199
Theorems, omega_of_Finite      362
Theorems, one_neutral_left      107
Theorems, orelse_example      63
Theorems, or_commutes      122
Theorems, pfact3      235
Theorems, plus_2_even_inv      247
Theorems, plus_2_even_inv’      249
Theorems, plus_assoc      162 433
Theorems, plus_assoc’      172
Theorems, plus_comm      273
Theorems, plus_n_Sm      272
Theorems, plus_plus’      274
Theorems, plus’_comm      274
Theorems, plus”_Sn_m      275
Theorems, pow_log_le      430
Theorems, pred_strong2_thl      260
Theorems, pred_thl      260
Theorems, prime37      205
Theorems, prime61      205
Theorems, prime_2333      437
Theorems, reflection_test      438
Theorems, reflection_test3      445
Theorems, reflection_test4      447
Theorems, reflection_test’      441
Theorems, reflection_test”      442
Theorems, refl_equal      98
Theorems, regroup      127
Theorems, rem_even_ge_interval      279
Theorems, rem_even_lt_interval      279
Theorems, rem_l_even_interval      278
Theorems, rem_l_l_interval      277
Theorems, rem_l_odd_interval      279
Theorems, rem_odd_ge_interval      279
Theorems, rem_odd_lt_interval      279
Theorems, resolution      97
Theorems, ring_example2      197
Theorems, ring_example3      197
Theorems, ring_example4      197
Theorems, ring_example5      207
Theorems, ring_example6      207
Theorems, ring_example7      208
Theorems, ring_examplel      197
Theorems, Rpos_div2_wf      413
Theorems, simpl_on_example      210
Theorems, simpl_pattern_example      189
Theorems, sorted2_inv      216
Theorems, sortedl_inv      216
Theorems, sorted_nat_123      215
Theorems, sort_eq      447
Theorems, sort_eq_2      447
Theorems, sqr_01      244
Theorems, strange_empty      184
Theorems, structured_intro_example2      226
Theorems, structured_intro_examplel      226
Theorems, sum_even      227
1 2 3
blank
Реклама
blank
blank
HR
@Mail.ru
       © Электронная библиотека попечительского совета мехмата МГУ, 2004-2024
Электронная библиотека мехмата МГУ | Valid HTML 4.01! | Valid CSS! О проекте