Typed Lambda Calculi and Applications: International Conference on Typed Lambda Calculi and Applications TLCA ’93 March, 16–18, 1993, Utrecht, The Netherlands Proceedings

حساب لامبدا در دهه 1930 توسط آلونزو چرچ توسعه یافت. حساب دیفرانسیل و انتگرال مدل جالبی از محاسبات بود و به نمونه اولیه زبان های برنامه نویسی تابعی نامشخص تبدیل شد. معناشناسی عملیاتی و معنایی برای حساب دیفرانسیل و انتگرال به عنوان مثالی برای سایر زبان های برنامه نویسی عمل کرد. در محاسبات لامبدا تایپ شده، اصطلاحات لامبدا بر اساس رفتار کاربردی آنها طبقه بندی می شوند. در دهه 1960 کشف شد که انواع محاسبات لامبدا تایپ شده در واقع ظاهری از گزاره های منطقی هستند. بنابراین دو دیدگاه ممکن از محاسبات لامبدا تایپ شده وجود دارد: - به عنوان مدل های محاسبات، که در آن اصطلاحات به عنوان برنامه در یک زبان برنامه نویسی تایپ شده مشاهده می شوند. - به عنوان نظریه های منطقی، که در آن انواع به عنوان گزاره و اصطلاحات به عنوان برهان در نظر گرفته می شوند. نتایج عملی این مطالعات عبارتند از: - زبان های برنامه نویسی تابعی که از نظر ریاضی مختصرتر از برنامه های ضروری هستند. - سیستم هایی برای بررسی خودکار اثبات بر اساس لامبدا کالولی. این جلد مجموعه مقالات TLCA '93، اولین کنفرانس بین المللی در محاسبات و کاربردهای تایپ شده لامبدا است که توسط گروه فلسفه دانشگاه اوترخت سازماندهی شده است. این شامل 29 مقاله انتخاب شده از 51 ارسال شده است.

The lambda calculus was developed in the 1930s by Alonzo Church. The calculus turned out to be an interesting model of computation and became theprototype for untyped functional programming languages. Operational and denotational semantics for the calculus served as examples for otherprogramming languages. In typed lambda calculi, lambda terms are classified according to their applicative behavior. In the 1960s it was discovered that the types of typed lambda calculi are in fact appearances of logical propositions. Thus there are two possible views of typed lambda calculi: - as models of computation, where terms are viewed as programs in a typed programming language; - as logical theories, where the types are viewed as propositions and the terms as proofs. The practical spin-off from these studies are: - functional programming languages which are mathematically more succinct than imperative programs; - systems for automated proof checking based on lambda caluli. This volume is the proceedings of TLCA '93, the first international conference on Typed Lambda Calculi and Applications,organized by the Department of Philosophy of Utrecht University. It includes29 papers selected from 51 submissions.