Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Two methods are studied for proving equivalence of programs involving two forms of information hiding. The proof methods are _logical relations_ and _bisimulations_; the forms of information hiding are _type abstraction_ and _perfect encryption_ (also known as _dynamic sealing_). Our thesis is that these theories are useful for reasoning about programs involving information hiding. We prove it through soundness and completeness theorems as well as examples including abstract data structures and cryptographic protocols. Type abstraction is the most foundational form of information hiding in programming languages. Logical relations are the primary method for reasoning about type abstraction, which is often called _relational parametricity_ or _representation independence_. Encryption is another foundational form of information hiding that is predominant in communication systems. In fact, an encryption-like primitive is useful for abstraction in programming languages as well, where it is called dynamic sealing. Given this intuitive connection between two forms of information hiding in computer software, it is natural to wonder whether we can establish more formal connections between them and transfer reasoning techniques from one to the other. We give affirmative answers to these questions. First, we adapt the theory of relational parametricity from type abstraction to dynamic sealing by defining a simply typed lambda-calculus extended with primitives for dynamic sealing, named lambda-seal-arrow, and its logical relations. As an illustrative application of this theory, we prove security properties of cryptographic protocols by means of careful encodings into the calculus. Second, we develop a theory of bisimulations for dynamic sealing. Unlike logical relations, it extends with no difficulty to richer languages with recursive functions, recursive types, or even no types at all. We illustrate its power by defining untyped lambda-calculus with dynamic sealing, which is named lambda-seal, and proving the equivalence of different implementations of abstract data structures as well as the correctness of a complex cryptographic protocol. Third, we ``feed back'' this theory of bisimulations from dynamic sealing to type abstraction to obtain the first sound, complete, and yet elementary theory of type abstraction in lambda-calculus with full universal, existential, and recursive types (called lambda-mu-all-exists). Our examples include abstract data types, generative functors, and an object encoding. We conclude with a conjecture of full abstraction for type-directed translation from type abstraction into dynamic sealing and with a possible direction for application to language environments supporting statically checked, dynamically checked, and unchecked programs at the same time without sacrificing abstraction.