دسترسی نامحدود
برای کاربرانی که ثبت نام کرده اند
برای ارتباط با ما می توانید از طریق شماره موبایل زیر از طریق تماس و پیامک با ما در ارتباط باشید
در صورت عدم پاسخ گویی از طریق پیامک با پشتیبان در ارتباط باشید
برای کاربرانی که ثبت نام کرده اند
درصورت عدم همخوانی توضیحات با کتاب
از ساعت 7 صبح تا 10 شب
دسته بندی: منطق ویرایش: نویسندگان: Yves Bertot. Pierre Castéran سری: Texts in Theoretical Computer Science. An EATCS Series ISBN (شابک) : 3540208542 ناشر: Springer سال نشر: 2004 تعداد صفحات: 498 زبان: English فرمت فایل : DJVU (درصورت درخواست کاربر به PDF، EPUB یا AZW3 تبدیل می شود) حجم فایل: 3 مگابایت
در صورت تبدیل فایل کتاب Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions به فرمت های PDF، EPUB، AZW3، MOBI و یا DJVU می توانید به پشتیبان اطلاع دهید تا فایل مورد نظر را تبدیل نمایند.
توجه داشته باشید کتاب اثبات قضیه تعاملی و توسعه برنامه: Coq'Art: حساب ساختارهای استقرایی نسخه زبان اصلی می باشد و کتاب ترجمه شده به فارسی نمی باشد. وبسایت اینترنشنال لایبرری ارائه دهنده کتاب های زبان اصلی می باشد و هیچ گونه کتاب ترجمه شده یا نوشته شده به فارسی را ارائه نمی دهد.
Coq یک دستیار اثبات تعاملی برای توسعه نظریه های ریاضی و نرم افزار رسمی تایید شده است. این نظریه مبتنی بر نظریه ای به نام حساب سازه های استقرایی است که گونه ای از نظریه نوع است. این کتاب مقدمه ای عملی برای توسعه اثبات ها و برنامه های تایید شده با استفاده از Coq ارائه می دهد. با مجموعه بزرگی از مثالها و تمرینها، ابزار ارزشمندی برای محققان، دانشجویان و مهندسان علاقهمند به روشهای رسمی و توسعه نرمافزار بدون خطا است.
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.