دانلود کتاب Adapting Proofs-as-Programs: The Curry-Howard Protocol (به فارسی: تطبیق مدارک به عنوان برنامه: پروتکل کری هاوارد) نوشته شده توسط «Iman Poernomo – John N. Crossley – Martin Wirsing»
اطلاعات کتاب تطبیق مدارک به عنوان برنامه: پروتکل کری هاوارد
موضوع اصلی: کامپیوترها
نوع: کتاب الکترونیکی
ناشر: Springer
نویسنده: Iman Poernomo – John N. Crossley – Martin Wirsing
زبان: English
فرمت کتاب: pdf (قابل تبدیل به سایر فرمت ها)
سال انتشار: 2005
تعداد صفحه: 416
حجم کتاب: 5 مگابایت
کد کتاب: 9780387237596 , 0387237593
توضیحات کتاب تطبیق مدارک به عنوان برنامه: پروتکل کری هاوارد
این تک‌نگاره چندین پیشرفت مهم در حوزه معروف به پارادایم اثبات به‌عنوان برنامه، مجموعه‌ای از رویکردها برای توسعه برنامه‌ها از اثبات‌ها در منطق سازنده را شرح می‌دهد. این هدف دوگانه ارائه یک نمای کلی پیشرفته از زمینه و جزئیات ابزارها و تکنیک ها برای تحریک تحقیقات بیشتر را دنبال می کند.
یکی از موضوعات اصلی کتاب یک چارچوب کلی و انتزاعی برای توسعه سیستم‌های جدید ترکیب برنامه با تطبیق اثبات‌ها به عنوان برنامه با زمینه‌های جدید است، که نویسندگان آن را پروتکل کری-هاوارد می‌نامند. این پروتکل برای ارائه دو برنامه کاربردی جدید برای مهندسی نرم افزار پیچیده در مقیاس صنعتی استفاده می شود: سنتز برنامه الزامی قراردادی و سنتز نرم افزار ساخت یافته. این برنامه ها توجیهی مثال زدنی برای کاربرد پروتکل در زمینه های مختلف است.
این کتاب برای دانشجویان فارغ التحصیل در علوم کامپیوتر یا ریاضیات در نظر گرفته شده است که مایلند پیشینه خود را در منطق و نظریه نوع و همچنین به دست آورند. تجربه کار با چارچوب های منطقی و سیستم های اثبات عملی. علاوه بر این، جامعه تحقیقاتی اثبات به عنوان برنامه و منطق محاسباتی گسترده‌تر، روش‌های رسمی و جوامع مهندسی نرم‌افزار سود خواهند برد. برنامه های کاربردی ارائه شده در کتاب باید برای محققانی که در حوزه های مشکل هدف کار می کنند مورد علاقه باشد.
This monograph details several important advances in the area known as the proofs-as-programs paradigm, a set of approaches to developing programs from proofs in constructive logic. It serves the dual purpose of providing a state-of-the-art overview of the field and detailing tools and techniques to stimulate further research.
One of the book’s central themes is a general, abstract framework for developing new systems of program synthesis by adapting proofs-as-programs to new contexts, which the authors call the Curry–Howard Protocol. This protocol is used to provide two novel applications for industrial-scale, complex software engineering: contractual imperative program synthesis and structured software synthesis. These applications constitute an exemplary justification for the applicability of the protocol to different contexts.
The book is intended for graduate students in computer science or mathematics who wish to extend their background in logic and type theory as well as gain experience working with logical frameworks and practical proof systems. In addition, the proofs-as-programs research community, and the wider computational logic, formal methods and software engineering communities will benefit. The applications given in the book should be of interest for researchers working in the target problem domains.
دانلود کتاب «تطبیق مدارک به عنوان برنامه: پروتکل کری هاوارد»
برای دریافت کد تخفیف ۲۰ درصدی این کتاب، ابتدا صفحه اینستاگرام کازرون آنلاین (@kazerun.online ) را دنبال کنید. سپس، کلمه «بلیان» را در دایرکت ارسال کنید تا کد تخفیف به شما ارسال شود.