کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
10118865 | 1633559 | 2005 | 47 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
Linear realizability and full completeness for typed lambda-calculi
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
موضوعات مرتبط
مهندسی و علوم پایه
ریاضیات
منطق ریاضی
پیش نمایش صفحه اول مقاله
![عکس صفحه اول مقاله: Linear realizability and full completeness for typed lambda-calculi Linear realizability and full completeness for typed lambda-calculi](/preview/png/10118865.png)
چکیده انگلیسی
We present the model construction technique called Linear Realizability. It consists in building a category of Partial Equivalence Relations over a Linear Combinatory Algebra. We illustrate how it can be used to provide models, which are fully complete for various typed λ-calculi. In particular, we focus on special Linear Combinatory Algebras of partial involutions, and we present PER models over them which are fully complete, inter alia, w.r.t. the following languages and theories: the fragment of System F consisting of ML-types, the maximal theory on the simply typed λ-calculus with finitely many ground constants, and the maximal theory on an infinitary version of this latter calculus.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Annals of Pure and Applied Logic - Volume 134, Issues 2â3, July 2005, Pages 122-168
Journal: Annals of Pure and Applied Logic - Volume 134, Issues 2â3, July 2005, Pages 122-168
نویسندگان
Samson Abramsky, Marina Lenisa,