A Bisimulation for Dynamic Sealing

Eijiro Sumii and Benjamin C. Pierce

To appear at Principles of Programming Languages (POPL04), Venice, Italy, January 14-16, 2004


We define lambda-seal, an untyped call-by-value lambda-calculus with primitives for _sealing_, and develop a bisimulation proof method that is sound and complete with respect to contextual equivalence. This provides a formal basis for reasoning about data abstraction in open, dynamic settings where static techniques such as type abstraction and logical relations are not applicable.

Server START Conference Manager
Update Time 19 Sep 2003 at 17:40:43
Maintainer Xavier.Leroy@inria.fr.
Start Conference Manager
Conference Systems