دسترسی نامحدود
برای کاربرانی که ثبت نام کرده اند
برای ارتباط با ما می توانید از طریق شماره موبایل زیر از طریق تماس و پیامک با ما در ارتباط باشید
در صورت عدم پاسخ گویی از طریق پیامک با پشتیبان در ارتباط باشید
برای کاربرانی که ثبت نام کرده اند
درصورت عدم همخوانی توضیحات با کتاب
از ساعت 7 صبح تا 10 شب
ویرایش: 1 نویسندگان: Gerwin Klein (auth.), Matt Kaufmann, Lawrence C. Paulson (eds.) سری: Lecture Notes in Computer Science 6172 : Theoretical Computer Science and General Issues ISBN (شابک) : 9783642140525, 3642140521 ناشر: Springer-Verlag Berlin Heidelberg سال نشر: 2010 تعداد صفحات: 505 زبان: English فرمت فایل : PDF (درصورت درخواست کاربر به PDF، EPUB یا AZW3 تبدیل می شود) حجم فایل: 5 مگابایت
کلمات کلیدی مربوط به کتاب اثبات قضیه تعاملی: اولین کنفرانس بین المللی، ITP 2010، ادینبورگ، انگلستان، 11-14 ژوئیه، 2010. مجموعه مقالات: منطق و معانی برنامه ها، مهندسی نرم افزار، منطق ریاضی و زبان های رسمی، زبان های برنامه نویسی، کامپایلرها، مترجمان، هوش مصنوعی (شامل رباتیک)، آنتی بادی ها
در صورت تبدیل فایل کتاب Interactive Theorem Proving: First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings به فرمت های PDF، EPUB، AZW3، MOBI و یا DJVU می توانید به پشتیبان اطلاع دهید تا فایل مورد نظر را تبدیل نمایند.
توجه داشته باشید کتاب اثبات قضیه تعاملی: اولین کنفرانس بین المللی، ITP 2010، ادینبورگ، انگلستان، 11-14 ژوئیه، 2010. مجموعه مقالات نسخه زبان اصلی می باشد و کتاب ترجمه شده به فارسی نمی باشد. وبسایت اینترنشنال لایبرری ارائه دهنده کتاب های زبان اصلی می باشد و هیچ گونه کتاب ترجمه شده یا نوشته شده به فارسی را ارائه نمی دهد.
Front Matter....Pages -
A Formally Verified OS Kernel. Now What?....Pages 1-7
Proof Assistants as Teaching Assistants: A View from the Trenches....Pages 8-8
A Certified Denotational Abstract Interpreter....Pages 9-24
Using a First Order Logic to Verify That Some Set of Reals Has No Lesbegue Measure....Pages 25-34
A New Foundation for Nominal Isabelle....Pages 35-50
(Nominal) Unification by Recursive Descent with Triangular Substitutions....Pages 51-66
A Formal Proof of a Necessary and Sufficient Condition for Deadlock-Free Adaptive Networks....Pages 67-82
Extending Coq with Imperative Features and Its Application to SAT Verification....Pages 83-98
A Tactic Language for Declarative Proofs....Pages 99-114
Programming Language Techniques for Cryptographic Proofs....Pages 115-130
Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder....Pages 131-146
Formal Proof of a Wave Equation Resolution Scheme: The Method Error....Pages 147-162
An Efficient Coq Tactic for Deciding Kleene Algebras....Pages 163-178
Fast LCF-Style Proof Reconstruction for Z3....Pages 179-194
The Optimal Fixed Point Combinator....Pages 195-210
Formal Study of Plane Delaunay Triangulation....Pages 211-226
Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison....Pages 227-242
A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture....Pages 243-258
Automated Machine-Checked Hybrid System Safety Proofs....Pages 259-274
Coverset Induction with Partiality and Subsorts: A Powerlist Case Study....Pages 275-290
Case-Analysis for Rippling and Inductive Proof....Pages 291-306
Importing HOL Light into Coq....Pages 307-322
A Mechanized Translation from Higher-Order Logic to Set Theory....Pages 323-338
The Isabelle Collections Framework....Pages 339-354
Interactive Termination Proofs Using Termination Cores....Pages 355-370
A Framework for Formal Verification of Compiler Optimizations....Pages 371-386
On the Formalization of the Lebesgue Integration Theory in HOL....Pages 387-402
From Total Store Order to Sequential Consistency: A Practical Reduction Theorem....Pages 403-418
Equations: A Dependent Pattern-Matching Compiler....Pages 419-434
A Mechanically Verified AIG-to-BDD Conversion Algorithm....Pages 435-449
Inductive Consequences in the Calculus of Constructions....Pages 450-465
Validating QBF Invalidity in HOL4....Pages 466-480
Higher-Order Abstract Syntax in Isabelle/HOL....Pages 481-484
Separation Logic Adapted for Proofs by Rewriting....Pages 485-489
Developing the Algebraic Hierarchy with Type Classes in Coq....Pages 490-493
Back Matter....Pages -