دانلود کتاب Interactive Theorem Proving: Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings
کتاب اثبات قضیه تعاملی: سومین کنفرانس بین المللی، ITP 2012، پرینستون، نیوجرسی، ایالات متحده آمریکا، 13-15 اوت 2012. مجموعه مقالات نسخه زبان اصلی
دانلود کتاب اثبات قضیه تعاملی: سومین کنفرانس بین المللی، ITP 2012، پرینستون، نیوجرسی، ایالات متحده آمریکا، 13-15 اوت 2012. مجموعه مقالات بعد از پرداخت مقدور خواهد بود
توضیحات کتاب در بخش جزئیات آمده است و می توانید موارد را مشاهده فرمایید
توضیحاتی در مورد کتاب Interactive Theorem Proving: Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings
نام کتاب : Interactive Theorem Proving: Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings
ویرایش : 1
عنوان ترجمه شده به فارسی : اثبات قضیه تعاملی: سومین کنفرانس بین المللی، ITP 2012، پرینستون، نیوجرسی، ایالات متحده آمریکا، 13-15 اوت 2012. مجموعه مقالات
سری : Lecture Notes in Computer Science 7406
نویسندگان : Lawrence C. Paulson (auth.), Lennart Beringer, Amy Felty (eds.)
ناشر : Springer-Verlag Berlin Heidelberg
سال نشر : 2012
تعداد صفحات : 428
ISBN (شابک) : 9783642323461 , 9783642323478
زبان کتاب : English
فرمت کتاب : pdf
حجم کتاب : 7 مگابایت
بعد از تکمیل فرایند پرداخت لینک دانلود کتاب ارائه خواهد شد. درصورت ثبت نام و ورود به حساب کاربری خود قادر خواهید بود لیست کتاب های خریداری شده را مشاهده فرمایید.
توضیحاتی در مورد کتاب :
این کتاب مجموعه مقالات کامل داوری شده سومین کنفرانس بین المللی اثبات قضیه تعاملی، ITP 2012، برگزار شده در پرینستون، نیوجرسی، ایالات متحده آمریکا، در آگوست 2012 است. گفتگوها و یک آموزش دعوت شده به دقت بررسی و از بین 40 مورد ارسالی انتخاب شد. از جمله موضوعات تحت پوشش رسمی سازی ریاضیات است. انتزاع برنامه و منطق. ساختار داده و سنتز؛ امنیت؛ (غیر) خاتمه و خودکار. تایید برنامه؛ قضیه اثبات توسعه; استدلال در مورد اجرای برنامه؛ و زیرساخت ها و سبک های مدل سازی را ارائه کنید.
فهرست مطالب :
Front Matter....Pages -
MetiTarski: Past and Future....Pages 1-10
Computer-Aided Cryptographic Proofs....Pages 11-27
A Differential Operator Approach to Equational Differential Invariants....Pages 28-48
Abella: A Tutorial....Pages 49-50
A Cantor Trio: Denumerability, the Reals, and the Real Algebraic Numbers....Pages 51-66
Construction of Real Algebraic Numbers in C oq ....Pages 67-82
A Refinement-Based Approach to Computational Algebra in Coq ....Pages 83-98
Bridging the Gap: Automatic Verified Abstraction of C....Pages 99-115
Abstract Interpretation of Annotated Commands....Pages 116-132
Verifying and Generating WP Transformers for Procedures on Complex Data....Pages 133-148
Bag Equivalence via a Proof-Relevant Membership Relation....Pages 149-165
Applying Data Refinement for Monadic Programs to Hopcroft’s Algorithm....Pages 166-182
Synthesis of Distributed Mobile Programs Using Monadic Types in Coq....Pages 183-200
Towards Provably Robust Watermarking....Pages 201-216
Priority Inheritance Protocol Proved Correct....Pages 217-232
Formalization of Shannon’s Theorems in SSReflect-Coq....Pages 233-249
Stop When You Are Almost-Full....Pages 250-265
Certification of Nontermination Proofs....Pages 266-282
A Compact Proof of Decidability for Regular Expression Equivalence....Pages 283-298
Using Locales to Define a Rely-Guarantee Temporal Logic....Pages 299-314
Charge!....Pages 315-331
Mechanised Separation Algebra....Pages 332-337
Directions in ISA Specification....Pages 338-344
More SPASS with Isabelle....Pages 345-360
A Language of Patterns for Subterm Selection....Pages 361-376
Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL....Pages 377-392
Proof Pearl: A Probabilistic Proof for the Girth-Chromatic Number Theorem....Pages 393-404
Standalone Tactics Using OpenTheory....Pages 405-411
Functional Programs: Conversions between Deep and Shallow Embeddings....Pages 412-417
Back Matter....Pages -
توضیحاتی در مورد کتاب به زبان اصلی :
This book constitutes the thoroughly refereed proceedings of the Third International Conference on Interactive Theorem Proving, ITP 2012, held in Princeton, NJ, USA, in August 2012. The 21 revised full papers presented together with 4 rough diamond papers, 3 invited talks, and one invited tutorial were carefully reviewed and selected from 40 submissions. Among the topics covered are formalization of mathematics; program abstraction and logics; data structures and synthesis; security; (non-)termination and automata; program verification; theorem prover development; reasoning about program execution; and prover infrastructure and modeling styles.
پست ها تصادفی