Internal models of system F for decompilation

详细信息	查看全文 | 推荐本文 |

• 作者：Stefano Berardi^a ; ^{stefano@di.unito.it} ; Makoto Tatsuta^b ; ^{tatsuta@nii.ac.jp}
• 关键词：Typed 位-calculus ; System F ; Semantics of polymorphism ; Compiler ; Decompiler ; de Bruijn level
• 刊名：Theoretical Computer Science
• 出版年：2012
• 期刊代码：114_03043975
• 类别：cp
• 出版时间：1 June, 2012
• 卷：435
• 期：Complete
• 页码：3-20
• 文件大小：376 K

摘要

This paper considers Girard鈥檚 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.