Главная    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
Предметный указатель
Certified programs, bdiv      409
Certified programs, Dict_Plus.addlist      340
Certified programs, Dict_Plus.build      340
Certified programs, div      417
Certified programs, div2_gen      255
Certified programs, div_bin2      281
Certified programs, div_bin3      282
Certified programs, div_F      416
Certified programs, div_it_terminates      422
Certified programs, eq_positive_dec      290
Certified programs, insert      320
Certified programs, le_rich_minus      395
Certified programs, list2tree      321
Certified programs, list2tree_aux      321
Certified programs, LKey.eqdec      333
Certified programs, log_domain_inv      429
Certified programs, More_Dec_Orders.le_lt_dec      336
Certified programs, naive_occ_dec      311
Certified programs, Nat_Order.le_eq_lt_dec      338
Certified programs, nested_F      419
Certified programs, occ_dec      317
Certified programs, PairKey.eqdec      333
Certified programs, pred_strong      260
Certified programs, pred_strong2      261
Certified programs, pred_strong2’      261
Certified programs, pred_strong2”      266
Certified programs, pred’      257
Certified programs, rmax      322
Certified programs, stronger_prime_test      264
Certified programs, TDict.add      344
Certified programs, TDict.empty      344
Certified programs, TDict.find      344
Certified programs, TrivialDict.add      341
Certified programs, TrivialDict.empty      341
Certified programs, TrivialDict.find      341
Certified programs, Zgt_bool’      303
Concepts, $\textit{Gallina}$      9
Concepts, Abstractions      25
Concepts, Alpha-conversion      28
Concepts, Axioms      46
Concepts, Bisimilarity      348 368
Concepts, Bisimulations      371
Concepts, Commands      13
Concepts, Comments      11
Concepts, Confluence      36
Concepts, Conjunction      219
Concepts, Constructors      138 142 153 167 171 187 214 350 379
Concepts, Contexts      19
Concepts, Convertibility order      39
Concepts, Curry-Howard isomorphism      44 82 211 390
Concepts, Delimiting keys      15
Concepts, Dependent product      73 105 137 211
Concepts, Dependent types      75 76 92
Concepts, Disjunction      219
Concepts, Environments      14 19
Concepts, Equality      98
Concepts, Equality, Heterogeneous equality      220
Concepts, Existential quantification      219
Concepts, Existential variables      111
Concepts, Expressions      14
Concepts, False elimination rule      97
Concepts, Fields      199
Concepts, Final type      53 108 141 191 245 379
Concepts, Functors      332
Concepts, Goals      46 47
Concepts, Groups      381
Concepts, Head types      53 108
Concepts, Higher-order functions      166
Concepts, Higher-order types      78
Concepts, Hypotheses      45
Concepts, Impredicative definitions      130
Concepts, Impredicativity      96
Concepts, Induction principle      382 388 392 404
Concepts, Instances      34
Concepts, Interpretation scopes      14 180
Concepts, Jokers      26 86
Concepts, Lemmas      46
Concepts, Linear inequalities      198 200
Concepts, Mathematical structures      156
Concepts, Minimal specification strengthening      261 303
Concepts, Module types (signatures)      326
Concepts, Modules      325
Concepts, Modules, parametric      332
Concepts, Normal forms      33
Concepts, Opacity      59
Concepts, Park principle      371
Concepts, Pattern matching      182
Concepts, Pattern matching, dependent      182 387 388
Concepts, Pattern matching, simultaneous      178
Concepts, Positivity (strict)      379
Concepts, Predicates      76 92
Concepts, Predicativity      96
Concepts, Principal premises      384
Concepts, Product typing triplets      92
Concepts, Programs      37
Concepts, Proof irrelevance      45 211 253 392
Concepts, Proof terms      45
Concepts, Propositions      45
Concepts, Quotient structures      156
Concepts, Realizations      41
Concepts, Recursion, principal argument      165
Concepts, Recursion, structural      165 266
Concepts, Recursion, well-founded      293 302 411
Concepts, Recursors      294 385 388 390 394 414
Concepts, Reduction sequences      36
Concepts, Rings      196
Concepts, Sections      19 30
Concepts, Signatures      326
Concepts, Simply typed $\lambda$-calculus      17
Concepts, Sorts      37
Concepts, Specifications      37
Concepts, Strong normalization      36
Concepts, Subgoals      46
Concepts, Subset types      252
Concepts, Substitutions      34
Concepts, Tacticals      61
Concepts, Tactics      3 41 46
Concepts, Tautologies      200
Concepts, Terms      14
Concepts, Theorems      46
Concepts, Transparency      59
Concepts, Type inference      26
Concepts, Type($i$)      38 40 45
Concepts, Types      14
Concepts, Types, inhabited types      20
Concepts, Typing judgments      20
Concepts, Universes      38
Concepts, Vernacular      9 13
Concepts, Well-founded relations      236 411
Function definitions, $t_{1}$      28
Function definitions, abscissa      145
Function definitions, absolute_fun      41
Function definitions, Acc_iter      294 399
Function definitions, ackermann      95
Function definitions, always_0      41
Function definitions, app      289
Function definitions, bad_get_prime      262
Function definitions, bdiv_aux      408
Function definitions, binary_word_duplicate      86
Function definitions, binomial      30 31
Function definitions, bin_A      443
Function definitions, bin_nat      440
Function definitions, bin_to_string      217
Function definitions, bin_to_string’      217
Function definitions, check_primality      436
Function definitions, check_primality’      436
Function definitions, check_range      436
Function definitions, check_range’      436
Function definitions, compose      87 89
Function definitions, count      400
Function definitions, cube      29
Function definitions, depth      380
Function definitions, div2      267 294
Function definitions, div2’      271
Function definitions, div2’_aux      271
Function definitions, divp_pair’      253
Function definitions, div_bin      277
Function definitions, div_it      424
Function definitions, div_it_F      421
Function definitions, example_dep_function      387
Function definitions, extract_option      431
Function definitions, flatten      439
Function definitions, flatten_aux      439
Function definitions, fright_son      170
Function definitions, from      352
Function definitions, from_marignan      41
Function definitions, fsum_all_values      171
Function definitions, general_omega      355
Function definitions, get_prime      264
Function definitions, htree_to_btree      182
Function definitions, insert_bin      446
Function definitions, insert_loop      305
Function definitions, insert_loop’      306
Function definitions, invert      183
Function definitions, iter      421
Function definitions, iterate      166
Function definitions, LAppend      354
Function definitions, LHead      351
Function definitions, list_to_vector      222
Function definitions, LList_decompose      358
Function definitions, LNth      351
Function definitions, log      429
Function definitions, log2      294 429
Function definitions, log2_aux      294
Function definitions, log2_aux_F      294
Function definitions, loopl’      303
Function definitions, LTail      351
Function definitions, max      425
Function definitions, month_length      142
Function definitions, mult2      164
Function definitions, mult2’      174 390
Function definitions, my_expo      95
Function definitions, my_mult      95
Function definitions, my_plus      95
Function definitions, nat_le_bool      445
Function definitions, nat_rec      389
Function definitions, nat_simple_rec      386
Function definitions, nb_seats      147
Function definitions, nb_wheels      147
Function definitions, next_month      151
Function definitions, nth_option      178
Function definitions, nth’      289
Function definitions, n_sum_all_values      171
Function definitions, n_sum_values      402
Function definitions, omega      355
Function definitions, opaque_f      115
Function definitions, or_to_nat      296
Function definitions, parse      232
Function definitions, plus      165
Function definitions, plus9      30
Function definitions, plus’      271
Function definitions, plus”      274
Function definitions, pred2      292
Function definitions, pred2_option      178
Function definitions, pred_option      178
Function definitions, pred_partial      258
Function definitions, pred_partial_2      260
Function definitions, pred_partial_2’      265
Function definitions, pred_partial’      265
Function definitions, pred’      292
Function definitions, projl’      100
Function definitions, Psucc      169 287
Function definitions, recognize      231
Function definitions, repeat      354
Function definitions, right_son      170
Function definitions, short_concat      90
Function definitions, sort_bin      446
Function definitions, square      197
Function definitions, Squares_from      352
Function definitions, sum_all_values      168
Function definitions, sum_n      174
Function definitions, thrice      89
Function definitions, to_marignan      41
Function definitions, trinomial      30 31
Function definitions, twice      85
Function definitions, two_power      430
Function definitions, t_delta      380
Function definitions, t_omega      380
Function definitions, update      397
Function definitions, vector_to_list      222
Function definitions, Zdist2      40
Function definitions, zero_present      168
Function definitions, Zsqr      34
Function definitions, Zsquare_diff      116
Function definitions, Z_btree_rec      391
Function definitions, Z_thrice      30
Libraries, Arith      20
Libraries, ArithRing      196
Libraries, Arrays      304
Libraries, Bool      20
Libraries, Bvector      222 223
Libraries, Classical      124 415
Libraries, JMeq      220 222-224
Libraries, List      77 102 175 222 377
Libraries, Omega      198
Libraries, Relations      132 212 369 415
Libraries, Streams      348
Libraries, Wellfounded      303 413
Libraries, Wf_nat      412 415
Libraries, ZArith      16 20 438
Libraries, ZArithRing      125 196
Libraries, Zwf      236
Modules and signatures, BoolKey      334
Modules and signatures, BoolKeys      334
Modules and signatures, DATA      340
Modules and signatures, DEC ORDER      335
Modules and signatures, DICT      339
Modules and signatures, DICT PLUS      328
Modules and signatures, Dictl      342
Modules and signatures, DictlPlus      342
Modules and signatures, Dict_Plus      340
Modules and signatures, KEY      329
Modules and signatures, Lexico      338
Modules and signatures, List_Order      339
Modules and signatures, LKey      333
Modules and signatures, LLZKey      333
Modules and signatures, LZKey      333
Modules and signatures, MOREDECORDERS      336
Modules and signatures, MoreNatNat      339
Modules and signatures, More_Dec_Orders      336
Modules and signatures, NatKey      332
Modules and signatures, NatNat      339
Modules and signatures, Nats      342
Modules and signatures, Nat_Order      338
Modules and signatures, PairKey      334
Modules and signatures, TDict      343
Modules and signatures, TrivialDict      341
Modules and signatures, ZKey      329
Modules and signatures, ZZKey      334
Plain definitions, bisimulation      371
Plain definitions, BoolKey.A      334
Plain definitions, classic      123
Plain definitions, deadlock      375
Plain definitions, de_morgan_not_and_not      123
Plain definitions, Dict_Plus.data      340
Plain definitions, Dict_Plus.dict      340
Plain definitions, Dict_Plus.key      340
Plain definitions, divides      203
Plain definitions, div_type      416
Plain definitions, div_type’      416
1 2 3
blank
Реклама
blank
blank
HR
@Mail.ru
       © Электронная библиотека попечительского совета мехмата МГУ, 2004-2025
Электронная библиотека мехмата МГУ | Valid HTML 4.01! | Valid CSS! О проекте