Category Theory and Computer Science: Paris, France, September 3–6, 1991 Proceedings

مقالات این جلد در چهارمین کنفرانس تابستانی دوسالانه نظریه مقوله و علوم کامپیوتر، که در پاریس برگزار شد، از 3 تا 6 سپتامبر 1991 ارائه شد. نظریه مقوله همچنان ابزار مهمی در مطالعات پایه در علوم کامپیوتر است. این به طور گسترده توسط منطق دانان برای بدست آوردن تفسیرهای مختصر از بسیاری از مفاهیم منطقی به کار گرفته شده است. اکنون بیش از بیست سال است که پیوندهای بین منطق و علوم کامپیوتر ایجاد شده است، به ویژه از طریق ایزومورفیسم کری هاوارد که برنامه ها را با برهان و انواع را با گزاره ها شناسایی می کند. نظریه مقوله مثلث - منطق - برنامه نویسی دنیایی غنی از ارتباطات متقابل را ارائه می دهد. موضوعات مطرح شده در این جلد شامل موارد زیر است. نظریه تیپ: قشربندی انواع و گزاره ها را می توان در یک محیط مقوله ای مورد بحث قرار داد. تئوری دامنه: نظریه دامنه ترکیبی نظریه دامنه را در درون جهان سازنده توپوس های مؤثر توسعه می دهد. منطق خطی: بازسازی منطق بر اساس گزاره ها به عنوان منابع به جایگزین هایی برای نحو سنتی منجر می شود. مجموعه مقالات سه کنفرانس تئوری دسته قبلی به عنوان یادداشت های سخنرانی در علوم کامپیوتر جلدهای 240، 283 و 389 ارائه می شود.

The papers in this volume were presented at the fourth biennial Summer Conference on Category Theory and Computer Science, held in Paris, September3-6, 1991. Category theory continues to be an important tool in foundationalstudies in computer science. It has been widely applied by logicians to get concise interpretations of many logical concepts. Links between logic and computer science have been developed now for over twenty years, notably via the Curry-Howard isomorphism which identifies programs with proofs and types with propositions. The triangle category theory - logic - programming presents a rich world of interconnections. Topics covered in this volume include the following. Type theory: stratification of types and propositions can be discussed in a categorical setting. Domain theory: synthetic domain theory develops domain theory internally in the constructive universe of the effective topos. Linear logic: the reconstruction of logic based on propositions as resources leads to alternatives to traditional syntaxes. The proceedings of the previous three category theory conferences appear as Lecture Notes in Computer Science Volumes 240, 283 and 389.