Молимо вас користите овај идентификатор за цитирање или овај линк до ове ставке:
https://open.uns.ac.rs/handle/123456789/11432
Назив: | Characterizing strong normalization in a language with control operators | Аутори: | Dougherty D. Gilezan, Silvia Lescanne P. |
Датум издавања: | 1-јан-2004 | Часопис: | Proceedings of the Sixth ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, PPDP'04 | Сажетак: | We investigate some fundamental properties of the reduction relation in the untyped term alculus derived from Curien and Herbelin's λμμ The original λμμ has a system of simple types, based on sequent calculus, embodying a Curry-Howard correspondence with classical logic; the significance of the untyped calculus of raw terms is that it is a Turing-complete language for computation with explicit representation of control as well as code. We define a type assignment system for the raw terms satisfying: a term is typable if and only if it is strongly normalizing. The intrinsic symmetry in the λμμ calculus leads to an essential use of both intersection and union types; in contrast to other union-types systems in the literature, our system enjoys the Subject Reduction property. | URI: | https://open.uns.ac.rs/handle/123456789/11432 | ISBN: | 1581138199 |
Налази се у колекцијама: | FTN Publikacije/Publications |
Приказати целокупан запис ставки
Преглед/и станица
83
Протекла недеља
31
31
Протекли месец
0
0
проверено 10.05.2024.
Google ScholarTM
Проверите
Алт метрика
Ставке на DSpace-у су заштићене ауторским правима, са свим правима задржаним, осим ако није другачије назначено.