Name
Abstract | ||
|---|---|---|
This paper considers Girard's internal coding of each term of System F by some term of a code type. This coding is the type-erasing coding definable already in the simply typed lambda-calculus using only abstraction on term variables. It is shown that there does not exist any decompiler for System F in System F, where the decompiler maps a term of System F to its code. An internal model of F is given by interpreting each type of F by some type equipped with maps between the type and the code type. This paper gives a decompiler-normalizer for this internal model in F, where the decompiler-normalizer maps any term of the internal model to the code of its normal form. It is also shown that for any model of F the composition of this internal model and the model produces another model of F whose equational theory is below untyped beta-eta-equality. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.1016/j.tcs.2012.02.022 | Theor. Comput. Sci. |
Keywords | DocType | Volume |
type-erasing coding definable,System F,code type,internal coding,decompiler map,internal model,decompiler-normalizer map,normal form,term variable,equational theory,system F | Journal | 435, |
ISSN | Citations | PageRank |
0304-3975 | 0 | 0.34 |
References | Authors | |
12 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Stefano Berardi | 1 | 373 | 51.58 |
| Makoto Tatsuta | 2 | 111 | 22.36 |