دسترسی نامحدود
برای کاربرانی که ثبت نام کرده اند
دانلود کتاب Interactive Theorem Proving: 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings
دانلود کتاب Theorem اثبات تعاملی: 5th کنفرانس بین المللی، ITP 2014، برگزار شد به عنوان بخشی از وین تابستان منطق، VSL 2014، وین، اتریش، 2014 ژوئیه 14-17. 2014. پرونده ها
مشخصات کتاب
Interactive Theorem Proving: 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings
ویرایش: 1
نویسندگان: Gerwin Klein. Ruben Gamboa (eds.)
سری: Lecture Notes in Computer Science 8558 Theoretical Computer Science and General Issues
ISBN (شابک) : 9783319089690, 9783319089706
ناشر: Springer International Publishing
سال نشر: 2014
تعداد صفحات: 572
زبان: English
فرمت فایل : PDF (درصورت درخواست کاربر به PDF، EPUB یا AZW3 تبدیل می شود)
حجم فایل: 8 مگابایت
قیمت کتاب (تومان) : 29,000
کلمات کلیدی مربوط به کتاب Theorem اثبات تعاملی: 5th کنفرانس بین المللی، ITP 2014، برگزار شد به عنوان بخشی از وین تابستان منطق، VSL 2014، وین، اتریش، 2014 ژوئیه 14-17. 2014. پرونده ها: منطق ریاضی و زبان های رسمی، هوش مصنوعی (شامل رباتیک)، منطق و معانی برنامه ها، مهندسی نرم افزار، سیستم ها و امنیت داده ها، تجزیه و تحلیل الگوریتم و پیچیدگی مسائل
در صورت تبدیل فایل کتاب Interactive Theorem Proving: 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings به فرمت های PDF، EPUB، AZW3، MOBI و یا DJVU می توانید به پشتیبان اطلاع دهید تا فایل مورد نظر را تبدیل نمایند.
توجه داشته باشید کتاب Theorem اثبات تعاملی: 5th کنفرانس بین المللی، ITP 2014، برگزار شد به عنوان بخشی از وین تابستان منطق، VSL 2014، وین، اتریش، 2014 ژوئیه 14-17. 2014. پرونده ها نسخه زبان اصلی می باشد و کتاب ترجمه شده به فارسی نمی باشد. وبسایت اینترنشنال لایبرری ارائه دهنده کتاب های زبان اصلی می باشد و هیچ گونه کتاب ترجمه شده یا نوشته شده به فارسی را ارائه نمی دهد.
توضیحاتی در مورد کتاب Theorem اثبات تعاملی: 5th کنفرانس بین المللی، ITP 2014، برگزار شد به عنوان بخشی از وین تابستان منطق، VSL 2014، وین، اتریش، 2014 ژوئیه 14-17. 2014. پرونده ها
این کتاب مجموعه مقالات پنجمین کنفرانس بین المللی اثبات قضیه تعاملی، ITP 2014، برگزار شده به عنوان بخشی از تابستان منطق وین، VSL 2014، در وین، اتریش، در ژوئیه 2014 است. 35 مقاله ارائه شده در این جلد از بین 59 مورد ارسالی به دقت بررسی و انتخاب شدند. موضوعات از مبانی نظری گرفته تا جنبه‌های اجرایی و کاربردها در تأیید برنامه، امنیت و رسمی‌سازی ریاضیات را شامل می‌شود.
توضیحاتی درمورد کتاب به خارجی
This book constitutes the proceedings of the 5th International Conference on Interactive Theorem Proving, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, in Vienna, Austria, in July 2014. The 35 papers presented in this volume were carefully reviewed and selected from 59 submissions. The topics range from theoretical foundations to implementation aspects and applications in program verification, security and formalization of mathematics.
فهرست مطالب
Front Matter....Pages -
Microcode Verification – Another Piece of the Microprocessor Verification Puzzle....Pages 1-16
Are We There Yet? 20 Years of Industrial Theorem Proving with SPARK....Pages 17-26
Towards a Formally Verified Proof Assistant....Pages 27-44
Implicational Rewriting Tactics in HOL....Pages 45-60
A Heuristic Prover for Real Inequalities....Pages 61-76
A Formal Library for Elliptic Curves in the Coq Proof Assistant....Pages 77-92
Truly Modular (Co)datatypes for Isabelle/HOL....Pages 93-110
Cardinals in Isabelle/HOL....Pages 111-127
Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code....Pages 128-143
Showing Invariance Compositionally for a Process Algebra for Network Protocols....Pages 144-159
A Computer-Algebra-Based Formal Proof of the Irrationality of ζ (3)....Pages 160-176
From Operational Models to Information Theory; Side Channels in pGCL with Isabelle....Pages 177-192
A Coq Formalization of Finitely Presented Modules....Pages 193-208
Formalized, Effective Domain Theory in Coq....Pages 209-225
Completeness and Decidability Results for CTL in Coq....Pages 226-241
Hypermap Specification and Certified Linked Implementation Using Orbits....Pages 242-257
A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction....Pages 258-274
Experience Implementing a Performant Category-Theory Library in Coq....Pages 275-291
A New and Formalized Proof of Abstract Completion....Pages 292-307
HOL with Definitions: Semantics, Soundness, and a Verified Implementation....Pages 308-324
Verified Efficient Implementation of Gabow’s Strongly Connected Component Algorithm....Pages 325-340
Recursive Functions on Lazy Lists via Domains and Topologies....Pages 341-357
Formal Verification of Optical Quantum Flip Gate....Pages 358-373
Compositional Computational Reflection....Pages 374-389
An Isabelle Proof Method Language....Pages 390-405
Proof Pearl: Proving a Simple Von Neumann Machine Turing Complete....Pages 406-420
The Reflective Milawa Theorem Prover Is Sound....Pages 421-436
Balancing Lists: A Proof Pearl....Pages 437-449
Unified Decision Procedures for Regular Expression Equivalence....Pages 450-466
Collaborative Interactive Theorem Proving with Clide....Pages 467-482
On the Formalization of Z-Transform in HOL....Pages 483-498
Universe Polymorphism in Coq ....Pages 499-514
Asynchronous User Interaction and Tool Integration in Isabelle/PIDE....Pages 515-530
HOL Constant Definition Done Right....Pages 531-536
Rough Diamond: An Extension of Equivalence-Based Rewriting....Pages 537-542
Formal C Semantics: CompCert and the C Standard....Pages 543-548
Mechanical Certification of Loop Pipelining Transformations: A Preview....Pages 549-554
Back Matter....Pages -
