دسترسی نامحدود
برای کاربرانی که ثبت نام کرده اند
دانلود کتاب Theorem Proving in Higher Order Logics: 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings
دانلود کتاب قضیه تئوری منطق سفارش بالاتر: 22 کنفرانس بین المللی، TPHOLs 2009، مونیخ، آلمان، 17-20 اوت 2009. پرونده ها
مشخصات کتاب
Theorem Proving in Higher Order Logics: 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings
ویرایش: 1 نویسندگان: David Basin, Srdjan Capkun, Patrick Schaller, Benedikt Schmidt (auth.), Stefan Berghofer, Tobias Nipkow, Christian Urban, Makarius Wenzel (eds.) سری: Lecture Notes in Computer Science 5674 : Theoretical Computer Science and General Issues ISBN (شابک) : 364203358X, 9783642033582 ناشر: Springer-Verlag Berlin Heidelberg سال نشر: 2009 تعداد صفحات: 527 زبان: English فرمت فایل : PDF (درصورت درخواست کاربر به PDF، EPUB یا AZW3 تبدیل می شود) حجم فایل: 6 مگابایت
قیمت کتاب (تومان) : 49,000
کلمات کلیدی مربوط به کتاب قضیه تئوری منطق سفارش بالاتر: 22 کنفرانس بین المللی، TPHOLs 2009، مونیخ، آلمان، 17-20 اوت 2009. پرونده ها: منطق ریاضی و زبان های رسمی، منطق و معانی برنامه ها، ریاضیات محاسبات، ریاضیات گسسته در علوم کامپیوتر، تجزیه و تحلیل الگوریتم و پیچیدگی مسائل، مدل ها و اصول
در صورت تبدیل فایل کتاب Theorem Proving in Higher Order Logics: 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings به فرمت های PDF، EPUB، AZW3، MOBI و یا DJVU می توانید به پشتیبان اطلاع دهید تا فایل مورد نظر را تبدیل نمایند.
توجه داشته باشید کتاب قضیه تئوری منطق سفارش بالاتر: 22 کنفرانس بین المللی، TPHOLs 2009، مونیخ، آلمان، 17-20 اوت 2009. پرونده ها نسخه زبان اصلی می باشد و کتاب ترجمه شده به فارسی نمی باشد. وبسایت اینترنشنال لایبرری ارائه دهنده کتاب های زبان اصلی می باشد و هیچ گونه کتاب ترجمه شده یا نوشته شده به فارسی را ارائه نمی دهد.
توضیحاتی در مورد کتاب قضیه تئوری منطق سفارش بالاتر: 22 کنفرانس بین المللی، TPHOLs 2009، مونیخ، آلمان، 17-20 اوت 2009. پرونده ها
این کتاب مجموعه مقالات داوری بیست و دومین کنفرانس بین‌المللی اثبات قضیه در منطق‌های مرتبه عالی، TPHOLs 200 است که در مونیخ، آلمان، در آگوست 2009 برگزار شد. 4 ارائه ابزار و 3 مقاله دعوت شده به دقت بررسی و از بین 55 مورد ارسالی انتخاب شدند.
مقالات تمام جنبه‌های اثبات قضیه در منطق‌های مرتبه بالاتر و همچنین موضوعات مرتبط در اثبات و تأیید قضیه مانند معناشناسی رسمی مشخصات، مدل‌سازی و زبان‌های برنامه‌نویسی، مشخصات و تأیید سخت‌افزار و نرم‌افزار را پوشش می‌دهند. رسمی‌سازی نظریه‌های ریاضی، پیشرفت‌ها در فناوری اثبات قضیه، و همچنین کاربرد صنعتی اثبات‌کننده‌های قضیه.
توضیحاتی درمورد کتاب به خارجی
This book constitutes the refereed proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, TPHOLs 200, held in Munich, Germany, in August 2009. The 26 revised full papers presented together with 1 proof pearl, 4 tool presentations, and 3 invited papers were carefully reviewed and selected from 55 submissions.
The papers cover all aspects of theorem proving in higher order logics as well as related topics in theorem proving and verification such as formal semantics of specification, modeling, and programming languages, specification and verification of hardware and software, formalization of mathematical theories, advances in theorem prover technology, as well as industrial application of theorem provers.
فهرست مطالب
Front Matter....Pages -
Let’s Get Physical: Models and Methods for Real-World Security Protocols....Pages 1-22
VCC: A Practical System for Verifying Concurrent C....Pages 23-42
Without Loss of Generality....Pages 43-59
HOL Light: An Overview....Pages 60-66
A Brief Overview of Mizar ....Pages 67-72
A Brief Overview of Agda – A Functional Language with Dependent Types....Pages 73-78
The Twelf Proof Assistant....Pages 79-83
Hints in Unification....Pages 84-98
Psi-calculi in Isabelle....Pages 99-114
Some Domain Theory and Denotational Semantics in Coq....Pages 115-130
Turning Inductive into Equational Specifications....Pages 131-146
Formalizing the Logic-Automaton Connection....Pages 147-163
Extended First-Order Logic....Pages 164-179
Formalising Observer Theory for Environment-Sensitive Bisimulation....Pages 180-195
Formal Certification of a Resource-Aware Language Implementation....Pages 196-211
A Certified Data Race Analysis for a Java-like Language....Pages 212-227
Formal Analysis of Optical Waveguides in HOL....Pages 228-243
The HOL-Omega Logic....Pages 244-259
A Purely Definitional Universal Domain....Pages 260-275
Types, Maps and Separation Logic....Pages 276-292
Acyclic Preferences and Existence of Sequential Nash Equilibria: A Formal and Constructive Equivalence....Pages 293-309
Formalising FinFuns – Generating Code for Functions as Data from Isabelle/HOL....Pages 310-326
Packaging Mathematical Structures....Pages 327-342
Practical Tactics for Separation Logic....Pages 343-358
Verified LISP Implementations on ARM, x86 and PowerPC....Pages 359-374
Trace-Based Coinductive Operational Semantics for While....Pages 375-390
A Better x86 Memory Model: x86-TSO....Pages 391-407
Formal Verification of Exact Computations Using Newton’s Method....Pages 408-423
Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL....Pages 424-439
A Hoare Logic for the State Monad....Pages 440-451
Certification of Termination Proofs Using CeTA ....Pages 452-468
A Formalisation of Smallfoot in HOL....Pages 469-484
Liveness Reasoning with Isabelle/HOL....Pages 485-499
Mind the Gap....Pages 500-515
Back Matter....Pages -
