Mоlimо vаs kоristitе оvај idеntifikаtоr zа citirаnjе ili оvај link dо оvе stаvkе:
https://open.uns.ac.rs/handle/123456789/14047
Nаziv: | Reducibility: A ubiquitous method in lambda calculus with intersection types | Аutоri: | Gilezan, Silvia Likavec S. |
Dаtum izdаvаnjа: | 1-феб-2003 | Čаsоpis: | Electronic Notes in Theoretical Computer Science | Sažetak: | A general reducibility method is developed for proving reduction properties of lambda terms typeable in intersection type systems with and without the universal type Ω. Sufficient conditions for its application are derived. This method leads to uniform proofs of confluence, standardization, weak head normalization of terms typeable in the system with the universal type Ω. The method extends Tait's reducibility method for the proof of strong normalization of the simply typed lambda calculus, Krivine's extension of the same method for the strong normalization of intersection type system without Ω, and Statman-Mitchell's logical relation method for the proof of confluence of β-η-reduction on the simply typed lambda terms. As a consequence, the confluence and the standardization of all (untyped) lambda terms is obtained. © 2002 Published by Elsevier Science B.V. | URI: | https://open.uns.ac.rs/handle/123456789/14047 | ISSN: | 15710661 | DOI: | 10.1016/S1571-0661(04)80493-6 |
Nаlаzi sе u kоlеkciјаmа: | FTN Publikacije/Publications |
Prikаzаti cеlоkupаn zаpis stаvki
SCOPUSTM
Nаvоđеnjа
2
prоvеrеnо 09.09.2023.
Prеglеd/i stаnicа
66
Prоtеklа nеdеljа
18
18
Prоtеkli mеsеc
2
2
prоvеrеnо 10.05.2024.
Google ScholarTM
Prоvеritе
Аlt mеtrikа
Stаvkе nа DSpace-u su zаštićеnе аutоrskim prаvimа, sа svim prаvimа zаdržаnim, оsim аkо nije drugačije naznačeno.