Academic Journal
Untangling Typechecking of Intersections and Unions
| العنوان: | Untangling Typechecking of Intersections and Unions |
|---|---|
| المؤلفون: | Joshua Dunfield |
| المصدر: | Electronic Proceedings in Theoretical Computer Science, Vol 45, Iss Proc. ITRS 2010, Pp 59-70 (2011) |
| بيانات النشر: | Open Publishing Association, 2011. |
| سنة النشر: | 2011 |
| المجموعة: | LCC:Mathematics LCC:Electronic computers. Computer science |
| مصطلحات موضوعية: | Mathematics, QA1-939, Electronic computers. Computer science, QA75.5-76.95 |
| الوصف: | Intersection and union types denote conjunctions and disjunctions of properties. Using bidirectional typechecking, intersection types are relatively straightforward, but union types present challenges. For union types, we can case-analyze a subterm of union type when it appears in evaluation position (replacing the subterm with a variable, and checking that term twice under appropriate assumptions). This technique preserves soundness in a call-by-value semantics. Sadly, there are so many choices of subterms that a direct implementation is not practical. But carefully transforming programs into let-normal form drastically reduces the number of choices. The key results are soundness and completeness: a typing derivation (in the system with too many subterm choices) exists for a program if and only if a derivation exists for the let-normalized program. |
| نوع الوثيقة: | article |
| وصف الملف: | electronic resource |
| اللغة: | English |
| تدمد: | 2075-2180 |
| Relation: | http://arxiv.org/pdf/1101.4428v1; https://doaj.org/toc/2075-2180 |
| DOI: | 10.4204/EPTCS.45.5 |
| URL الوصول: | https://doaj.org/article/46d5cce111524b4188cf886fcf2813a1 |
| رقم الانضمام: | edsdoj.46d5cce111524b4188cf886fcf2813a1 |
| قاعدة البيانات: | Directory of Open Access Journals |
Full Text Finder | تدمد: | 20752180 |
|---|---|
| DOI: | 10.4204/EPTCS.45.5 |