کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
4950019 1440354 2017 20 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
The Polarized λ-calculus
کلمات کلیدی
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
The Polarized λ-calculus
چکیده انگلیسی

A natural deduction system isomorphic to the focused sequent calculus for polarized intuitionistic logic is proposed. The system comes with a language of proof-terms, named polarized λ-calculus, whose reduction rules express simultaneously a normalization procedure and the isomorphic copy of the cut-elimination procedure pertaining to the focused sequent calculus. Noteworthy features of this natural deduction system are: how the polarity of a connective determines the style of its elimination rule; the existence of a proof-search strategy which is equivalent to focusing in the sequent calculus; the highly-disciplined organization of the syntax - even atoms have introduction, elimination and normalization rules. The polarized λ-calculus is a programming formalism close to call-by-push-value, but justified by its proof-theoretical pedigree.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Electronic Notes in Theoretical Computer Science - Volume 332, 11 June 2017, Pages 149-168
نویسندگان
,