|
Formal Methods in Computing (Most of the papers antecedent to 1995 are not included in the list) |
|||
| FRAMES NO FRAME | ||||
| BDDCdL15 (In proceedings) | |
| Author(s) | Jan Bessai, Boris Düdder, Andrej Dudenhefner, Tzu-Chun Chen and Ugo de' Liguoro |
| Title | « Typing Classes and Mixins with Intersection Types » |
| In | Proceedings Seventh Workshop on Intersection Types and Related Systems, Vienna, Austria, 18 July 2014 |
| Series | Electronic Proceedings in Theoretical Computer Science |
| Editor(s) | Jakob Rehof |
| Volume | 177 |
| Page(s) | 79-93 |
| Year | 2015 |
| Publisher | Open Publishing Association |
| Abstract | |
| We study an assignment system of intersection types for a lambda-calculus with records and a record- merge operator, where types are preserved both under subject reduction and expansion. The calculus is expressive enough to naturally represent mixins as functions over recursively defined classes, whose fixed points, the objects, are recursive records. In spite of the double recursion that is involved in their definition, classes and mixins can be meaningfully typed without resorting to neither recursive nor F-bounded polymorphic types. We then adapt mixin construct and composition to Java and C#, relying solely on existing features in such a way that the resulting code remains typable in the respective type systems. We exhibit some example code, and study its typings in the intersection type system via interpretation into the lambda-calculus with records we have proposed. | |
Download the complete article:
| BibTeX code |
@inproceedings{BDDCdL15,
volume = {177},
author = {Bessai, Jan and D\"udder, Boris and Dudenhefner, Andrej and Chen,
Tzu-Chun and de' Liguoro, Ugo},
series = {Electronic Proceedings in Theoretical Computer Science},
booktitle = {{\rm Proceedings Seventh Workshop on} Intersection Types and
Related Systems, {\rm Vienna, Austria, 18 July 2014}},
editor = {Rehof, Jakob},
title = {Typing Classes and Mixins with Intersection Types},
abstract = {We study an assignment system of intersection types for a
lambda-calculus with records and a record- merge operator, where
types are preserved both under subject reduction and expansion.
The calculus is expressive enough to naturally represent mixins as
functions over recursively defined classes, whose fixed points,
the objects, are recursive records. In spite of the double
recursion that is involved in their definition, classes and mixins
can be meaningfully typed without resorting to neither recursive
nor F-bounded polymorphic types. We then adapt mixin construct and
composition to Java and C\#, relying solely on existing features
in such a way that the resulting code remains typable in the
respective type systems. We exhibit some example code, and study
its typings in the intersection type system via interpretation
into the lambda-calculus with records we have proposed.},
tag = {ITRS'14},
localfile = {http://arxiv.org/abs/1503.04911},
publisher = {Open Publishing Association},
doi = {10.4204/EPTCS.177.7},
pages = {79-93},
year = {2015},
}
|
Formal Methods in Computing (Most of the papers antecedent to 1995 are not included in the list) |
|||
| FRAMES NO FRAME | ||||
This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)
