A new calculus of contexts

ABSTRACT

We study contexts (terms with holes) by proposing a 'λ-calculus with holes'. It is very expressive and can encode programming constructs apparently unrelated to contexts, including objects and algorithms in partial evaluation. We give proofs of confluence, preservation of strong normalisation, principal typing for an ML-style Hindley-Milner type system, and an applicative characterisation of contextual equivalence. We explore the limitations of the calculus including further applications, and discuss how they might be tackled.

REFERENCES

• 1: Martín Abadi , Luca Cardelli, An Imperative Object Calculus, Proceedings of the 6th International Joint Conference CAAP/FASE on Theory and Practice of Software Development, p.471-485, May 22-26, 1995
• 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: H. P. Barendregt, The lambda calculus: its syntax and semantics (revised ed.), Studies in Logic and the Foundations of Mathematics, vol. 103, North-Holland, 1984.
• 4: John Bell and Moshé Machover, A course in mathematical logic, North-Holland, 1977.
• 5: Gavin Bierman , Michael Hicks , Peter Sewell , Gareth Stoyle , Keith Wansbrough, Dynamic rebinding for marshalling and update, with destruct-time ?, Proceedings of the eighth ACM SIGPLAN international conference on Functional programming, p.99-110, August 25-29, 2003, Uppsala, Sweden
• 6: Roel Bloo and Kristoffer Høgsbro Rose, Preservation of strong normalisation in named lambda calculi with explicit substitution and garbage collection, CSN-95: Computer Science in the Netherlands, 1995.
• 7: Mirna Bognar, Contexts in lambda calculus, Ph.D. thesis, Vrije Universiteit Amsterdam, 2002.
• 8: Charles Consel and Olivier Danvy, Partial evaluation: Principles and perspectives, Journées Francophones des Langages Applicatifs, February 1993, pp. 493--501.
• 9: Luis Damas , Robin Milner, Principal type-schemes for functional programs, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.207-212, January 25-27, 1982, Albuquerque, Mexico [doi>10.1145/582153.582176]
• 10: Laurent Dami, A lambda-calculus for dynamic binding, Theoretical Computer Science, v.192 n.2, p.201-231, Feb. 20, 1998 [doi>10.1016/S0304-3975(97)00150-3]
• 11: Maribel Fernández and Murdoch J. Gabbay, Extensions of nominal rewriting, PPDP, 2005.
• 12: Murdoch J. Gabbay, a-logic, Submitted, 2005.
• 13: Murdoch J. Gabbay and A. M. Pitts, A new approach to abstract syntax with variable binding, Formal Aspects of Computing 13 (2001), 341--363.
• 14: M. Hamana, Free sigma-monoids: A higher-order syntax with metavariables, The Second Asian Symposium on Programming Languages and Systems (APLAS 2004), Lecture Notes in Computer Science, vol. 3202, 2004, pp. 348--363.
• 15: Masatomo Hashimoto , Atsushi Ohori, A typed context calculus, Theoretical Computer Science, v.266 n.1-2, p.249-272, 09/06/2001 [doi>10.1016/S0304-3975(00)00174-2]
• 16: Peyton Jones, Tackling the awkward squad: monadic input/output, concurrency, exceptions, and foreign-language calls in haskell, Engineering theories of software construction, Marktoberdorf Summer School, NATO ASI, 105 Press, 2001, pp. 47--96.
• 17: Simon L. Peyton Jones , Philip Wadler, Imperative functional programming, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.71-84, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158524]
• 18: John Launchbury , Simon L. Peyton Jones, Lazy functional state threads, Proceedings of the ACM SIGPLAN 1994 conference on Programming language design and implementation, p.24-35, June 20-24, 1994, Orlando, Florida, United States
• 19: Pierre Lescanne, From λσ to λν: a journey through calculi of explicit substitutions, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.60-69, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.174707]
• 20: Elena Machkasova , Franklyn A. Turbak, A Calculus for Link-Time Compilation, Proceedings of the 9th European Symposium on Programming Languages and Systems, p.260-274, April 02, 2000
• 21: Ian Mackie Maribel Fernández, Murdoch J. Gabbay, Nominal rewriting, Submitted, January 2004.
• 22: Masahiko Sato , Takafumi Sakurai , Rod Burstall, Explicit environments, Fundamenta Informaticae, v.45 n.1,2, p.79-115, Jan.2001
• 23: Dale Miller, A logic programming language with Lambda-abstraction, function variables, and simple unification, Proceedings of the international workshop on Extensions of logic programming, p.253-281, February 1991, Tu¨bingen, Germany
• 24: Robin Milner , Joachim Parrow , David Walker, A calculus of mobile processes, II, Information and Computation, v.100 n.1, p.41-77, Sept. 1992 [doi>10.1016/0890-5401(92)90009-5]
• 25: Eugenio Moggi, Notions of computation and monads, Information and Computation, v.93 n.1, p.55-92, July 1991 [doi>10.1016/0890-5401(91)90052-4]
• 26: Eugenio Moggi , Walid Taha , Zine-El-Abidine Benaissa , Tim Sheard, An Idealized MetaML: Simpler, and More Expressive, Proceedings of the 8th European Symposium on Programming Languages and Systems, p.193-207, March 22-28, 1999
• 27: Larry Paulson, The Isabelle reference manual, Cambridge University Computer Laboratory, February 2001.
• 28: A. M. Pitts and T. Sheard, On the denotational semantics of staged execution of open code, Submitted, February 2004.
• 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: Masahiko Sato , Takafumi Sakurai , Yukiyoshi Kameyama, A Simply Typed Context Calculus with First-Class Environments, Proceedings of the 5th International Symposium on Functional and Logic Programming, p.359-374, March 07-09, 2001
• 31: Masahiko Sato, Takafumi Sakurai, Yukiyoshi Kameyama, and Atsushi Igarashi, Calculi of meta-variables, Computer Science Logic and 8th Kurt Gödel Colloquium (CSL'03 & KGC), Vienna, Austria. Proccedings (M. Baaz, ed.), Lecture Notes in Computer Science, vol. 2803, 2003, pp. 484--497.
• 32: Tim Sheard , Simon Peyton Jones, Template meta-programming for Haskell, Proceedings of the 2002 ACM SIGPLAN workshop on Haskell, p.1-16, October 03, 2002, Pittsburgh, Pennsylvania [doi>10.1145/581690.581691]
• 33: Francois Maurel Sylvain Baro, The qnu and qnuk calculi: name capture and control, Tech. report, Université Paris VII, March 2003, Extended Abstract, Prépublication PPS//03/11//n°16.
• 34: Laurence Tratt, Compile-time meta-programming in converge, Tech. Report TR-04-11, Department of Computer Science, King's College London, December 2002.
• 35: Christian Urban , Andrew M. Pitts , Murdoch J. Gabbay, Nominal unification, Theoretical Computer Science, v.323 n.1-3, p.473-497, 14 September 2004 [doi>10.1016/j.tcs.2004.06.016]
• 36: Vincent van Oostrom, Confluence for abstract and higher-order rewriting, Ph.D. thesis, Vrije Universiteit, Amsterdam, March 29 1994.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

General Terms:
Theory

Keywords:
binders, calculi of contexts, functional programming, lambda-calculi, nominal techniques