Theorem Proving in Higher Order Logics: 14th International Conference, TPHOLs 2001 Edinburgh, Scotland, UK, September 3–6, 2001 Proceedings

این جلد مجموعه مقالات چهاردهمین کنفرانس بین‌المللی اثبات قضیه در منطق‌های مرتبه عالی (TPHOLs 2001) است که از 3 تا 6 سپتامبر 2001 در ادینبورگ، اسکاتلند برگزار شد. TPHOLs تمام جنبه های اثبات قضیه در منطق های مرتبه بالاتر و همچنین موضوعات مرتبط در اثبات و راستی آزمایی قضیه را پوشش می دهد. TPHOLs 2001 با یازدهمین کنفرانس کاری تحقیقاتی پیشرفته در مورد طراحی صحیح سخت افزار و روش های تأیید صحت (CHARME 2001) همراه شد. این جلسه در 4 تا 7 سپتامبر 2001 در نزدیکی لیوینگستون، اسکاتلند در مؤسسه یکپارچه سازی سطح سیستم برگزار شد و یک جلسه نیم روزه مشترک مذاکرات برای 5 سپتامبر در ادینبورگ ترتیب داده شد. سفری به خانه تراکور و ضیافتی در کتابخانه پلیفیر کالج اولد، دانشگاه ادینبورگ نیز به طور مشترک برگزار شد. مجموعه مقالات CHARME 2001 به عنوان جلد 2144 از مجموعه یادداشت‌های سخنرانی Springer-Verlag در علوم کامپیوتر با تیزیانا مارگاریا و تام ملهام به عنوان ویراستاران منتشر شده است. هر یک از 47 مقاله ارسال شده در گروه تحقیق کامل توسط حداقل 3 داور که توسط کمیته برنامه انتخاب شده بودند، داوری شدند. از این تعداد، 23 مورد برای ارائه در کنفرانس و انتشار در این جلد پذیرفته شد. مطابق با سنت، TPHOLs 2001 همچنین مکانی را برای ارائه کارهای در دست اجرا ایجاد کرد، جایی که محققان با استفاده از یک سخنرانی مقدماتی مختصر به بحث دعوت می‌کنند و سپس در یک جلسه پوستر درباره کار خود بحث می‌کنند. مجموعه مقالات تکمیلی حاوی مقالات مرتبط برای کار در حال پیشرفت توسط بخش انفورماتیک در دانشگاه ادینبورگ منتشر شد.

This volume constitutes the proceedings of the 14th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2001) held 3–6 September 2001 in Edinburgh, Scotland. TPHOLs covers all aspects of theorem proving in higher order logics, as well as related topics in theorem proving and veri?cation. TPHOLs 2001 was collocated with the 11th Advanced Research Working Conference on Correct Hardware Design and Veri?cation Methods (CHARME 2001). This was held 4–7 September 2001 in nearby Livingston, Scotland at the Institute for System Level Integration, and a joint half-day session of talks was arranged for the 5th September in Edinburgh. An excursion to Traquair House and a banquet in the Playfair Library of Old College, University of Edinburgh were also jointly organized. The proceedings of CHARME 2001 have been p- lished as volume 2144 of Springer-Verlag’s Lecture Notes in Computer Science series, with Tiziana Margaria and Tom Melham as editors. Each of the 47 papers submitted in the full research category was refereed by at least 3 reviewers who were selected by the Program Committee. Of these submissions, 23 were accepted for presentation at the conference and publication in this volume. In keeping with tradition, TPHOLs 2001 also o?ered a venue for the presentation of work in progress, where researchers invite discussion by means of a brief preliminary talk and then discuss their work at a poster session. A supplementary proceedings containing associated papers for work in progress was published by the Division of Informatics at the University of Edinburgh.