دسترسی نامحدود
برای کاربرانی که ثبت نام کرده اند
دانلود کتاب Certified Programs and Proofs: First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings
دانلود کتاب برنامه ها و اثبات های مجاز: اولین کنفرانس بین المللی ، CPP 2011 ، کنتینگ ، تایوان ، 7-9 دسامبر 2011. مجموعه مقالات
مشخصات کتاب
Certified Programs and Proofs: First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings
ویرایش: 1 نویسندگان: Nikolaj Bjørner (auth.), Jean-Pierre Jouannaud, Zhong Shao (eds.) سری: Lecture Notes in Computer Science 7086 Theoretical Computer Science and General Issues ISBN (شابک) : 9783642253799, 3642253792 ناشر: Springer-Verlag Berlin Heidelberg سال نشر: 2011 تعداد صفحات: 414 زبان: English فرمت فایل : PDF (درصورت درخواست کاربر به PDF، EPUB یا AZW3 تبدیل می شود) حجم فایل: 4 مگابایت
قیمت کتاب (تومان) : 35,000
کلمات کلیدی مربوط به کتاب برنامه ها و اثبات های مجاز: اولین کنفرانس بین المللی ، CPP 2011 ، کنتینگ ، تایوان ، 7-9 دسامبر 2011. مجموعه مقالات: منطق و معانی برنامه ها، منطق ریاضی و زبان های رسمی، زبان های برنامه نویسی، کامپایلر، مفسر، دستکاری نمادین و جبری، مهندسی نرم افزار، هوش مصنوعی (شامل رباتیک)
در صورت تبدیل فایل کتاب Certified Programs and Proofs: First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings به فرمت های PDF، EPUB، AZW3، MOBI و یا DJVU می توانید به پشتیبان اطلاع دهید تا فایل مورد نظر را تبدیل نمایند.
توجه داشته باشید کتاب برنامه ها و اثبات های مجاز: اولین کنفرانس بین المللی ، CPP 2011 ، کنتینگ ، تایوان ، 7-9 دسامبر 2011. مجموعه مقالات نسخه زبان اصلی می باشد و کتاب ترجمه شده به فارسی نمی باشد. وبسایت اینترنشنال لایبرری ارائه دهنده کتاب های زبان اصلی می باشد و هیچ گونه کتاب ترجمه شده یا نوشته شده به فارسی را ارائه نمی دهد.
توضیحاتی در مورد کتاب برنامه ها و اثبات های مجاز: اولین کنفرانس بین المللی ، CPP 2011 ، کنتینگ ، تایوان ، 7-9 دسامبر 2011. مجموعه مقالات
این کتاب مجموعه مقالات ارجاعی اولین کنفرانس بین‌المللی برنامه‌ها و شواهد گواهی شده، CPP 2011، برگزار شده در کنتینگ، تایوان، در دسامبر 2011 است. و از بین 49 مورد ارسالی انتخاب شد. آنها در بخش‌های موضوعی در مورد منطق و انواع، گواهی‌ها، رسمی‌سازی، دستیاران اثبات، تدریس، زبان‌های برنامه‌نویسی، گواهی‌نامه سخت‌افزار، متفرقه، و پرل‌های اثبات سازماندهی شده‌اند.
توضیحاتی درمورد کتاب به خارجی
This book constitutes the referred proceedings of the First
International Conference on Certified Programs and Proofs,
CPP 2011, held in Kenting, Taiwan, in December 2011.
The 24 revised regular papers presented together with 4
invited talks were carefully reviewed and selected from 49
submissions. They are organized in topical sections on logic
and types, certificates, formalization, proof assistants,
teaching, programming languages, hardware certification,
miscellaneous, and proof perls.
فهرست مطالب
Front Matter....Pages -
Engineering Theories with Z3....Pages 1-2
Algebra, Logic, Locality, Concurrency....Pages 3-4
Constructive Formalization of Hybrid Logic with Eventualities....Pages 5-20
Proof-Carrying Code in a Session-Typed Process Calculus....Pages 21-36
Automated Certification of Implicit Induction Proofs....Pages 37-53
A Proposal for Broad Spectrum Proof Certificates....Pages 54-69
Univalent Semantics of Constructive Type Theories....Pages 70-70
Formalization of Wu’s Simple Method in Coq....Pages 71-86
Reasoning about Constants in Nominal Isabelle or How to Formalize the Second Fixed Point Theorem....Pages 87-102
Simple, Functional, Sound and Complete Parsing for All Context-Free Grammars....Pages 103-118
A Decision Procedure for Regular Expression Equivalence in Type Theory....Pages 119-134
A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses....Pages 135-150
Modular SMT Proofs for Fast Reflexive Checking Inside Coq....Pages 151-166
Tactics for Reasoning Modulo AC in Coq....Pages 167-182
Reconstruction of Z3’s Bit-Vector Proofs in HOL4 and Isabelle/HOL....Pages 183-198
Teaching Experience: Logic and Formal Methods with Coq....Pages 199-215
The Teaching Tool CalcCheck A Proof-Checker for Gries and Schneider’s “Logical Approach to Discrete Math”....Pages 216-230
VeriSmall: Verified Smallfoot Shape Analysis....Pages 231-246
Verification of Scalable Synchronous Queue ....Pages 247-263
Coq Mechanization of Featherweight Fortress with Multiple Dispatch and Multiple Inheritance....Pages 264-279
Mechanizing the Metatheory of mini-XQuery....Pages 280-295
Automatically Verifying Typing Constraints for a Data Processing Language....Pages 296-313
Hardware-Dependent Proofs of Numerical Programs....Pages 314-329
Coquet: A Coq Library for Verifying Hardware....Pages 330-345
First Steps towards the Certification of an ARM Simulator Using Compcert....Pages 346-361
Full Reduction at Full Throttle....Pages 362-377
Certified Security Proofs of Cryptographic Protocols in the Computational Model: An Application to Intrusion Resilience....Pages 378-393
Proof Pearl: The Marriage Theorem....Pages 394-399
Back Matter....Pages -
نظرات کاربران
کتاب های تصادفی
دانلود کتاب Blue Wizard Is About To Die! Prose, Poems, and Emoto-Versatronic Expressionist Pieces About Video Games (1980-2003)
