ABSTRACT
We introduce a new notion of bisimulation for showing contextual equivalence of expressions in an untyped lambda-calculus with an explicit store, and in which all expressed values, including higher-order values, are storable. Our notion of bisimulation leads to smaller and more tractable relations than does the method of Sumii and Pierce [31]. In particular, our method allows one to write down a bisimulation relation directly in cases where [31] requires an inductive specification, and where the principle of local invariants [22] is inapplicable. Our method can also express examples with higher-order functions, in contrast with the most widely known previous methods [4, 22, 32] which are limited in their ability to deal with such examples. The bisimulation conditions are derived by manually extracting proof obligations from a hypothetical direct proof of contextual equivalence.
- Samson Abramsky. The lazy lambda calculus. In David~A. Turner, editor, Research Topics in Functional Programming, pages 65--116. Addison-Wesley, 1990. Google ScholarDigital Library
- Samson Abramsky, Radha Jagadeesan, and Pasquale Malacaria. Full abstraction for PCF. Inf. Comput., 163(2):409--470, 2000. Originally appeared as {3}. Google ScholarDigital Library
- Samson Abramsky, Pasquale Malacaria, and Radha Jagadeesan. Full abstraction for PCF. In Theoretical Aspects of Computer Software, pages 1--15, 1994. Google ScholarDigital Library
- Nick Benton and Benjamin Leperchey. Relational reasoning in a nominal semantics for storage. In Typed Lambda Calculi and Applications, 7th International Conference, TLCA 2005, Nara, Japan, April 21-23, 2005, Proceedings, volume 3461 of Lecture Notes in Computer Science, pages 86--101. Springer, 2005. Google ScholarDigital Library
- Martin Berger, Kohei Honda, and Nobuko Yoshida. A logical analysis of aliasing in imperative higher-order functions. In Proceedings of the Tenth ACM SIGPLAN International Conference on Functional Programming (ICFP'05). ACM Press, sept 2005. To appear. Google ScholarDigital Library
- Yuxin Deng and Davide Sangiorgi. Towards an algebraic theory of typed mobile processes. In Proc. Icalp '04, volume 3142 of Lecture Notes in Computer Science, pages 445--456. Springer-Verlag, 2004.Google Scholar
- Matthias Felleisen. The Calculi of Lambda-v-cs Conversion: A Syntactic Theory of Control and State in Imperative Higher-Order Programming Languages. PhD thesis, Indiana University, 1987. Google ScholarDigital Library
- Cormac Flanagan and Matthias Felleisen. The semantics of future and its use in program optimization. In Proceedings 22nd Annual ACM Symposium on Principles of Programming Languages, pages 209--220, 1995. Google ScholarDigital Library
- Matthew Hennessy. Algebraic theory of processes. MIT Press, Cambridge, MA, USA, 1988. Google ScholarDigital Library
- Matthew Hennessy and Robin Milner. On observing nondeterminism and concurrency. In ICALP, pages 299--309, 1980. Google ScholarDigital Library
- Matthew Hennessy and Robin Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 32:137--161, 1985. Google ScholarDigital Library
- Kohei Honda, Martin Berger, and Nobuko Yoshida. An observationally complete program logic for imperative higher-order functions. In Proceedings of the Twentieth Annual IEEE Symposium on Logic in Computer Science (LICS), June 2005. To appear. Google ScholarDigital Library
- Douglas J. Howe. Equality in lazy computation systems. In Proc. 4th IEEE Symposium on Logic in Computer Science, pages 198--203, 1989. Google ScholarDigital Library
- R. Jagadeesan, A. S. A. Jeffrey, and J. Riely. A calculus of untyped aspect-oriented programs. In Proceedings European Conference on Object-Oriented Programming, volume 1853 of Lecture Notes in Computer Science, pages 415--427, Berlin, Heidelberg, and New York, 2003. Springer-Verlag.Google ScholarCross Ref
- Eugene M. Kohlbecker and Mitchell Wand. Macro-by-example: Deriving syntactic transformations from their specifications. In Proceedings 14th Annual ACM Symposium on Principles of Programming Languages, pages 77--84, 1987. Google ScholarDigital Library
- Ian A. Mason and Carolyn L. Talcott. Equivalence in functional languages with effects. Journal of Functional Programming, 1:287--327, 1991.Google ScholarCross Ref
- Albert R. Meyer and Kurt Sieber. Towards fully abstract semantics for local variables: Preliminary report. In Proceedings 15th Annual ACM Symposium on Principles of Programming Languages, pages 191--203, 1988. Google ScholarDigital Library
- Robert Milne and Christopher Strachey. A Theory of Programming Language Semantics. Chapman and Hall, London, 1976. Also Wiley, New York. Google ScholarDigital Library
- Robin Milner. Fully abstract models of typed lambda-calculi. Theoretical Computer Science, 4:1--22, 1977.Google ScholarCross Ref
- Robin Milner. Operational and algebraic semantics of concurrent processes. In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science, pages 1201--1242. MIT Press/Elsevier, 1990. Google ScholarDigital Library
- James H. Morris, Jr. Lambda Calculus Models of Programming Languages. PhD thesis, MIT, Cambridge, MA, 1968.Google Scholar
- Andrew Pitts and Ian Stark. Operational reasoning for functions with local state. In Andrew Gordon and Andrew Pitts, editors, Higher Order Operational Techniques in Semantics, pages 227--273. Publications of the Newton Institute, Cambridge University Press, 1998. Google ScholarDigital Library
- Gordon D. Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5:223--255, 1977.Google ScholarCross Ref
- E. Ritter and A. M. Pitts. A fully abstract translation between a γ-calculus with reference types and Standard ML. In 2nd Int. Conf. on Typed Lambda Calculus and Applications, Edinburgh, 1995, volume 902 of Lecture Notes in Computer Science, pages 397--413, Berlin, Heidelberg, and New York, 1995. Springer-Verlag. Google ScholarDigital Library
- Davide Sangiorgi. Locality and true-concurrency in calculi for mobile processes. In Theoretical Aspects of Computer Software, pages 405--424, 1994. Google ScholarDigital Library
- Davide Sangiorgi. On the bisimulation proof method. In J. Wiedermann and P. Háiek, editors, Proc. MFCS'95, volume 969 of Lecture Notes in Computer Science, pages 479--488. Springer-Verlag, 1995. Full version to appear in J. Math. Structures in Comp. Sci. Google ScholarDigital Library
- Davide Sangiorgi. Locality and non-interleaving semantics in calculi for mobile processes. Theoretical Computer Science, 155:39--83, 1996. Google ScholarDigital Library
- Davide Sangiorgi and Robin Milner. The problem of "Weak Bisimulation up to". In W.R. Cleveland, editor, Proc. CONCUR '92, volume 630 of Lecture Notes in Computer Science, pages 32--46. Springer-Verlag, 1992. Google ScholarDigital Library
- Kurt Sieber. Full abstraction for the second order subset of an algol-like language. Theor. Comput. Sci., 168(1):155--212, 1996. Google ScholarDigital Library
- Paul A. Steckler and Mitchell Wand. Lightweight closure conversion. ACM Transactions on Programming Languages and Systems, 19(1):48--86, January 1997. Original version appeared in Proceedings 21st Annual ACM Symposium on Principles of Programming Languages, 1994. Google ScholarDigital Library
- Eijiro Sumii and Benjamin C. Pierce. A bisimulation for dynamic sealing. In POPL '04: Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 161--172, New York, NY, USA, 2004. ACM Press. Google ScholarDigital Library
- Eijiro Sumii and Benjamin C. Pierce. A bisimulation for type abstraction and recursion. In POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 63--74, New York, NY, USA, 2005. ACM Press. Google ScholarDigital Library
- Jerzy Tiuryn and Mitchell Wand. Untyped lambda-calculus with input-output. In H. Kirchner, editor, Trees in Algebra and Programming: CAAP'96, Proc. 21st International Colloquium, volume 1059 of Lecture Notes in Computer Science, pages 317--329, Berlin, Heidelberg, and New York, April 1996. Springer-Verlag. Google ScholarDigital Library
- Mitchell Wand and William~D. Clinger. Set constraints for destructive array update optimization. Journal of Functional Programming, 11(3):319--346, May 2001. Google ScholarDigital Library
- Mitchell Wand and Igor Siveroni. Constraint systems for useless variable elimination. In Proceedings 26th Annual ACM Symposium on Principles of Programming Languages, pages 291--302, 1999. Google ScholarDigital Library
- Mitchell Wand and Gregory T. Sullivan. Denotational semantics using an operationally-based term model. In Proceedings 23rd Annual ACM Symposium on Principles of Programming Languages, pages 386--399, 1997. Google ScholarDigital Library
Index Terms
- Small bisimulations for reasoning about higher-order imperative programs
Recommendations
Environmental bisimulations for higher-order languages
Developing a theory of bisimulation in higher-order languages can be hard. Particularly challenging can be: (1) the proof of congruence, as well as enhancements of the bisimulation proof method with “up-to context” techniques, and (2) obtaining ...
Small bisimulations for reasoning about higher-order imperative programs
Proceedings of the 2006 POPL ConferenceWe introduce a new notion of bisimulation for showing contextual equivalence of expressions in an untyped lambda-calculus with an explicit store, and in which all expressed values, including higher-order values, are storable. Our notion of bisimulation ...
Environmental bisimulations for probabilistic higher-order languages
POPL '16Environmental bisimulations for probabilistic higher-order languages are studied. In contrast with applicative bisimulations, environmental bisimulations are known to be more robust and do not require sophisticated techniques such as Howe’s in the ...
Comments