Proof and Computation

مفاهیم و روش‌های منطقی در بسیاری از زمینه‌های علوم کامپیوتر اهمیت فزاینده‌ای دارند. پارادایم اثبات به عنوان برنامه و پذیرش گسترده Prolog این را به وضوح نشان می دهد. مفهوم منطقی یک اثبات رسمی در سیستم های سازنده مختلف را می توان به عنوان یک روش بسیار صریح برای توصیف یک روش محاسباتی در نظر گرفت. همچنین برعکس، توسعه سیستم های منطقی تحت تأثیر انباشت دانش در مورد تکنیک های بازنویسی و یکسان سازی قرار گرفته است. این جلد شامل مجموعه‌ای از سخنرانی‌های محققان برجسته است که ایده‌های جدیدی را در مورد تأثیر مفهوم اثبات رسمی بر نظریه محاسبات ارائه می‌کنند. موضوعات تحت پوشش عبارتند از: مشخصات و انواع داده های انتزاعی، تکنیک های اثبات، روش های سازنده، منطق خطی، و همزمانی و منطق.

Logical concepts and methods are of growing importance in many areas of computer science. The proofs-as-programs paradigm and the wide acceptance of Prolog show this clearly. The logical notion of a formal proof in various constructive systems can be viewed as a very explicit way to describe a computation procedure. Also conversely, the development of logical systems has been influenced by accumulating knowledge on rewriting and unification techniques. This volume contains a series of lectures by leading researchers giving a presentation of new ideas on the impact of the concept of a formal proof on computation theory. The subjects covered are: specification and abstract data types, proving techniques, constructive methods, linear logic, and concurrency and logic.