000200246 001__ 200246
000200246 005__ 20190316235942.0
000200246 037__ $$aREP_WORK
000200246 245__ $$aAdditional Material for "Unifying Data Representation Transformations"
000200246 269__ $$a2014
000200246 260__ $$c2014
000200246 336__ $$aReports
000200246 520__ $$aThis report shows an attempt to formalize the data representation transformation mechanism in the ``Unifying Data Representation Transformations'' paper. Since the mechanism described in the paper is targeted at the Scala programming language and the specification is written against System Fsub with local colored type inference formally reasoning about the calculus is a major undertaking. Instead, in this report we start from the simply typed lambda calculus with subtyping, natural numbers and unit. We add rewriting and adapt the calculus to propagate expected type information in a mechanism inspired from local colored type inference. Finally we show how the representation transformation mechanism (the convert phase) rewrites terms. We show that, given a series of assumptions about the inject phase, type-checking a term against the updated rules produces a correct and operationally equivalent term, with a minimum number of runtime coercions introduced for the annotations given. We finish the report by giving a series of examples which show how the code is transformed.
000200246 700__ $$0245399$$aUreche, Vlad$$g200717
000200246 8564_ $$s873525$$uhttps://infoscience.epfl.ch/record/200246/files/ldl-form.pdf$$yn/a$$zn/a
000200246 8564_ $$s72651$$uhttps://infoscience.epfl.ch/record/200246/files/ldl-logo.png$$yn/a$$zn/a
000200246 909C0 $$0252187$$pLAMP$$xU10409
000200246 909CO $$ooai:infoscience.tind.io:200246$$pIC$$preport$$qGLOBAL_SET
000200246 917Z8 $$x200717
000200246 917Z8 $$x200717
000200246 917Z8 $$x200717
000200246 917Z8 $$x200717
000200246 917Z8 $$x200717
000200246 937__ $$aEPFL-REPORT-200246
000200246 973__ $$aEPFL
000200246 980__ $$aREPORT