A complete, co-inductive syntactic theory of sequential control and state

ABSTRACT

We present a new co-inductive syntactic theory, eager normal form bisimilarity, for the untyped call-by-value lambda calculus extended with continuations and mutable references.We demonstrate that the associated bisimulation proof principle is easy to use and that it is a powerful tool for proving equivalences between recursive imperative higher-order programs.The theory is modular in the sense that eager normal form bisimilarity for each of the calculi extended with continuations and/or mutable references is a fully abstract extension of eager normal form bisimilarity for its sub-calculi. For each calculus, we prove that eager normal form bisimilarity is a congruence and is sound with respect to contextual equivalence. Furthermore, for the calculus with both continuations and mutable references, we show that eager normal form bisimilarity is complete: it coincides with contextual equivalence.

REFERENCES

• 1: Samson Abramsky, The lazy lambda calculus, Research topics in functional programming, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1990
• 2: S. Abramsky , K. Honda , G. McCusker, A Fully Abstract Game Semantics for General References, Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science, p.334, June 21-24, 1998
• 3: Z. M. Ariola and H. Herbelin. Minimal classical logic and control operators. In ICALP, volume 2719 of Lecture Notes in Computer Science, pages 871--885. Springer-Verlag, 2003.
• 4: H. P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. Number 103 in Studies in Logic and the Foundations of Mathematics. North-Holland, revised edition, 1984.
• 5: Gavin M. Bierman, A Computational Interpretation of the lambda-µ-Calculus, Proceedings of the 23rd International Symposium on Mathematical Foundations of Computer Science, p.336-345, August 24-28, 1998
• 6: R. David and W. Py. λμ-calculus and Böhm's theorem. Journal of Symbolic Logic, 66(1):407--413, 2001.
• 7: Lavinia Egidi , Furio Honsell , Simona Ronchi Della Rocca, Operational, denotational and logical descriptions: a case study, Fundamenta Informaticae, v.16 n.2, p.149-169, Feb. 1992
• 8: Matthias Felleisen , Robert Hieb, The revised report on the syntactic theories of sequential control and state, Theoretical Computer Science, v.103 n.2, p.235-271, 14 Sept. 1992 [doi>10.1016/0304-3975(92)90014-7]
• 9: Daniel P. Friedman , Christopher T. Haynes, Constraining control, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.245-254, January 14-16, 1985, New Orleans, Louisiana, United States [doi>10.1145/318593.318654]
• 10: Andrew D. Gordon, Bisimilarity as a theory of functional programming, Theoretical Computer Science, v.228 n.1-2, p.5-47, Oct. 1999 [doi>10.1016/S0304-3975(98)00353-3]
• 11: Andrew D. Gordon , Andrew M. Pitts, Higher order operational techniques in semantics, Cambridge University Press, New York, NY, 1999
• 12: Philippe de Groote, On the Relation between the Lambda-Mu-Calculus and the Syntactic Theory of Sequential Control, Proceedings of the 5th International Conference on Logic Programming and Automated Reasoning, p.31-43, July 16-22, 1994
• 13: Vasileios Koutavas , Mitchell Wand, Small bisimulations for reasoning about higher-order imperative programs, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.141-152, January 11-13, 2006, Charleston, South Carolina, USA
• 14: James Laird, Full abstraction for functional languages with control, Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science, p.58, June 29-July 02, 1997
• 15: P. J. Landin. The mechanical evaluation of expressions. The Computer Journal, 6(4):308--320, 1964.
• 16: S. B. Lassen. Bisimulation up to context for imperative lambda calculus. Unpublished note. Presented at emphThe Semantic Challenge of Object-Oriented Programming, Schloss Dagstuhl, 1998.
• 17: S. B. Lassen, Relational reasoning about contexts, Higher order operational techniques in semantics, Cambridge University Press, New York, NY, 1999
• 18: S. B. Lassen. Bisimulation in untyped lambda calculus: Böhm trees and bisimulation up to context. In MFPS XV, volume 20 of Electronic Notes in Theoretical Computer Science, pages 346--374. Elsevier, 1999.
• 19: Soren Lassen, Eager Normal Form Bisimulation, Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science (LICS' 05), p.345-354, June 26-29, 2005 [doi>10.1109/LICS.2005.15]
• 20: S. B. Lassen. Normal form simulation for McCarty's amb. In MFPS XXI, volume 155 of Electronic Notes in Theoretical Computer Science, pages 445--465. Elsevier, 2005.
• 21: Soren B. Lassen, Head Normal Form Bisimulation for Pairs and the \lambda\mu-Calculus, Proceedings of the 21st Annual IEEE Symposium on Logic in Computer Science, p.297-306, August 12-15, 2006 [doi>10.1109/LICS.2006.29]
• 22: P. B. Levy. Game semantics using function inventories. Talk given at emphGeometry of Computation 2006, Marseille, 2006.
• 23: I. A. Mason and C. L. Talcott. Equivalence in functional languages with effects. Journal of Functional Programming, 1(3):297--327, 1991.
• 24: M. Merro and C. Biasi. On the observational theory of the CPS-calculus (extended abstract). In Proc. 22nd Conference on Mathematical Foundations of Programming Semantics, volume 158 of Electronic Notes in Theoretical Computer Science, pages 307--330. Elsevier, 2006.
• 25: A. R. Meyer , K. Sieber, Towards fully abstract semantics for local variables, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.191-203, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73577]
• 26: Michel Parigot, Lambda-My-Calculus: An Algorithmic Interpretation of Classical Natural Deduction, Proceedings of the International Conference on Logic Programming and Automated Reasoning, p.190-201, July 15-20, 1992
• 27: R. P. Perez. An extensional partial combinatory algebra based on λ-terms. In A. Tarlecki, editor, Proc. Mathematical Foundations of Computer Science, volume 520 of Lecture Notes in Computer Science, pages 387--396. Springer-Verlag, 1991.
• 28: A. M. Pitts, Reasoning about local variables with operationally-based logical relations, Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, p.152, July 27-30, 1996
• 29: A. M. Pitts , I. D. B. Stark, Operational reasoning for functions with local state, Higher order operational techniques in semantics, Cambridge University Press, New York, NY, 1999
• 30: Eike Ritter , Andrew M. Pitts, A Fully Abstract Translation between a Lambda-Calculus with Reference Types and Standard ML, Proceedings of the Second International Conference on Typed Lambda Calculi and Applications, p.397-413, April 10-12, 1995
• 31: Davide Sangiorgi, The lazy Lambda calculus in a concurrency scenario, Information and Computation, v.111 n.1, p.120-153, May 15 1994 [doi>10.1006/inco.1994.1042]
• 32: Eijiro Sumii , Benjamin C. Pierce, A bisimulation for type abstraction and recursion, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.63-74, January 12-14, 2005, Long Beach, California, USA
• 33: C. Talcott, Reasoning about functions with effects, Higher order operational techniques in semantics, Cambridge University Press, New York, NY, 1999
• 34: Mitchell Wand , Gregory T. Sullivan, Denotational semantics using an operationally-based term model, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.386-399, January 15-17, 1997, Paris, France [doi>10.1145/263699.263755]

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Control structures

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Operational semantics
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

General Terms:
Languages, Theory

Keywords:
bisimulation, continuations, mutable references