COMPUTER SCIENCE TECHNICAL REPORT ABSTRACTS

Source: http://reports-archive.adm.cs.cmu.edu/anon/1999/abstracts/99-100.html Parent: https://www.cs.cmu.edu/~fox/publications.html


	CMU-CS-99-100 Computer Science Department School of Computer Science, Carnegie Mellon University --- CMU-CS-99-100 Simple, Efficient Object Encoding using Intersection Karl Crary January 1999 Also appears as CMU-CS-FOX-99-01 CMU-CS-99-100.ps CMU-CS-99-100.pdf Keywords: Object encodings, intersection types, type theory I present a type-theoretic encoding of objects that interprets method dispatch by self-application (i.e., method functions are applied to the objects containing them) but still validates the expected subtyping relationships. The naive typing of self-application fails to validate the expected subtyping relationships because it is too permissive and allows application to similarly typed objects that are not self. This new encoding solves this problem by constraining methods to be applied only to self using existential and intersection types. Using this typing, I give a full account of objects including self types and method update. The typing constructs used in this encoding appear to be quite rich, but they may be axiomatized in a novel, restricted fashion that is metatheoretically simple. 20 pages
--- Return to: SCS Technical Report Collection School of Computer Science homepage This page maintained by reports@cs.cmu.edu

CMU-CS-99-100 Computer Science Department School of Computer Science, Carnegie Mellon University --- CMU-CS-99-100 Simple, Efficient Object Encoding using Intersection Karl Crary January 1999 Also appears as CMU-CS-FOX-99-01 CMU-CS-99-100.ps CMU-CS-99-100.pdf Keywords: Object encodings, intersection types, type theory I present a type-theoretic encoding of objects that interprets method dispatch by self-application (i.e., method functions are applied to the objects containing them) but still validates the expected subtyping relationships. The naive typing of self-application fails to validate the expected subtyping relationships because it is too permissive and allows application to similarly typed objects that are not self. This new encoding solves this problem by constraining methods to be applied only to self using existential and intersection types. Using this typing, I give a full account of objects including self types and method update. The typing constructs used in this encoding appear to be quite rich, but they may be axiomatized in a novel, restricted fashion that is metatheoretically simple. 20 pages

--- Return to: SCS Technical Report Collection School of Computer Science homepage This page maintained by reports@cs.cmu.edu