دسترسی نامحدود
برای کاربرانی که ثبت نام کرده اند
برای ارتباط با ما می توانید از طریق شماره موبایل زیر از طریق تماس و پیامک با ما در ارتباط باشید
در صورت عدم پاسخ گویی از طریق پیامک با پشتیبان در ارتباط باشید
برای کاربرانی که ثبت نام کرده اند
درصورت عدم همخوانی توضیحات با کتاب
از ساعت 7 صبح تا 10 شب
ویرایش: 1 نویسندگان: Robin Adams, Zhaohui Luo (auth.), Thorsten Altenkirch, Conor McBride (eds.) سری: Lecture Notes in Computer Science 4502 Theoretical Computer Science and General Issues ISBN (شابک) : 9783540744634, 9783540744641 ناشر: Springer-Verlag Berlin Heidelberg سال نشر: 2007 تعداد صفحات: 276 زبان: English فرمت فایل : PDF (درصورت درخواست کاربر به PDF، EPUB یا AZW3 تبدیل می شود) حجم فایل: 4 مگابایت
کلمات کلیدی مربوط به کتاب انواع اثبات و برنامه ها: کارگاه بین المللی ، انواع 2006 ، ناتینگهام ، انگلیس ، 18 تا 21 آوریل 2006 ، مقالات منتخب بازبینی شده: منطق و معانی برنامه ها، منطق ریاضی و زبان های رسمی، زبان های برنامه نویسی، کامپایلر، مفسر، دستکاری نمادین و جبری، هوش مصنوعی (شامل رباتیک)
در صورت تبدیل فایل کتاب Types for Proofs and Programs: International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers به فرمت های PDF، EPUB، AZW3، MOBI و یا DJVU می توانید به پشتیبان اطلاع دهید تا فایل مورد نظر را تبدیل نمایند.
توجه داشته باشید کتاب انواع اثبات و برنامه ها: کارگاه بین المللی ، انواع 2006 ، ناتینگهام ، انگلیس ، 18 تا 21 آوریل 2006 ، مقالات منتخب بازبینی شده نسخه زبان اصلی می باشد و کتاب ترجمه شده به فارسی نمی باشد. وبسایت اینترنشنال لایبرری ارائه دهنده کتاب های زبان اصلی می باشد و هیچ گونه کتاب ترجمه شده یا نوشته شده به فارسی را ارائه نمی دهد.
کارگاه بین المللی گروه کاری انواع در ناتینگهام، انگلستان، در آوریل 2006 برگزار شد. این کارگاه ذهن های برجسته در زمینه محاسبات و برنامه نویسی کامپیوتر را به خود جلب کرد که برای به اشتراک گذاشتن یافته های خود و بحث در مورد آخرین پیشرفت ها و برنامه های کاربردی در این زمینه آمده بودند. این کارگاه به عنوان بخشی از هفتمین سمپوزیوم گرایش های برنامه نویسی کاربردی برگزار شد. این کتاب پس از داوری کارگاه را تشکیل می دهد.
داخل این جلد 17 مقاله کامل است. هر یک از آنها به دقت مورد بررسی قرار گرفت و از بین 29 مورد ارسالی انتخاب شد.
این مقالات به تمام مسائل جاری در استدلال رسمی و برنامهنویسی رایانه بر اساس تئوری نوع، از جمله زبانها و ابزارهای رایانهای برای استدلال میپردازند. برنامه های کاربردی در چندین حوزه، مانند تجزیه و تحلیل زبان های برنامه نویسی. نرم افزار تایید شده؛ رسمی کردن ریاضیات؛ و آموزش ریاضی.
The International Workshop of the Types Working Group was held in Nottingham, UK, in April 2006. This workshop attracted leading minds in computing and computer programming who came to share their findings and discuss the latest developments and applications in the field. The workshop took place as part of the Seventh Symposium on Trends in Functional Programming. This book constitutes the refereed post-proceedings of the workshop.
Inside this volume are 17 full papers. Each one of them was carefully reviewed and selected from among 29 submissions.
The papers address all current issues in formal reasoning and computer programming based on type theory, including languages and computerized tools for reasoning; applications in several domains, such as analysis of programming languages; certified software; formalization of mathematics; and mathematics education.
Front Matter....Pages -
Weyl’s Predicative Classical Mathematics as a Logic-Enriched Type Theory....Pages 1-17
Crafting a Proof Assistant....Pages 18-32
On Constructive Cut Admissibility in Deduction Modulo....Pages 33-47
Fast Reflexive Arithmetic Tactics the Linear Case and Beyond....Pages 48-62
Combining de Bruijn Indices and Higher-Order Abstract Syntax in Coq....Pages 63-77
Deciding Equality in the Constructor Theory....Pages 78-92
A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family....Pages 93-109
Truth Values Algebras and Proof Normalization....Pages 110-124
Curry-Style Types for Nominal Terms....Pages 125-139
(In)consistency of Extensions of Higher Order Logic and Type Theory....Pages 140-159
Constructive Type Classes in Isabelle....Pages 160-174
Zermelo’s Well-Ordering Theorem in Type Theory....Pages 175-187
A Finite First-Order Theory of Classes....Pages 188-202
Coinductive Correctness of Homographic and Quadratic Algorithms for Exact Real Numbers....Pages 203-220
Using Intersection Types for Cost-Analysis of Higher-Order Polymorphic Functional Programs....Pages 221-236
Subset Coercions in Coq ....Pages 237-252
A Certified Distributed Security Logic for Authorizing Code....Pages 253-268
Back Matter....Pages -