Loading...
Please wait, while we are loading the content...
Similar Documents
Typed closure conversion preserves observational equivalence (2008)
| Content Provider | CiteSeerX |
|---|---|
| Author | Ahmed, Amal Blume, Matthias |
| Description | Language-based security relies on the assumption that all potential attacks are bound by the rules of the language in question. When programs are compiled into a different language, this is true only if the translation process preserves observational equivalence. We investigate the problem of fully abstract compilation, i.e., compilation that both preserves and reflects observational equivalence. In particular, we prove that typed closure conversion for the polymorphic λ-calculus with existential and recursive types is fully abstract. Our proof uses operational techniques in the form of a step-indexed logical relation and construction of certain wrapper terms that “back-translate ” from target values to source values. Although typed closure conversion has been assumed to be fully abstract, we are not aware of any previous result that actually proves this. 1 In ICFP |
| File Format | |
| Language | English |
| Publisher Date | 2008-01-01 |
| Access Restriction | Open |
| Subject Keyword | Operational Technique Language-based Security Relies Abstract Compilation Translation Process Typed Closure Conversion Certain Wrapper Term Recursive Type Previous Result Different Language Source Value Observational Equivalence Step-indexed Logical Relation Potential Attack Closure Conversion Target Value Polymorphic Calculus |
| Content Type | Text |
| Resource Type | Article |
