200246
20190316235942.0
REP_WORK
Additional Material for "Unifying Data Representation Transformations"
2014
2014
Reports
This 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.
Ureche, Vlad
200717
245399
n/a
873525
n/a
http://infoscience.epfl.ch/record/200246/files/ldl-form.pdf
n/a
72651
n/a
http://infoscience.epfl.ch/record/200246/files/ldl-logo.png
LAMP
252187
U10409
oai:infoscience.tind.io:200246
report
IC
GLOBAL_SET
200717
200717
200717
200717
200717
EPFL-REPORT-200246
EPFL
REPORT