Context-based proofs of termination for typed delimited-control operators

ABSTRACT

We present direct proofs of termination of evaluation for typed delimited-control operators shift and reset using a variant of Tait's method with context-based reducibility predicates. We address both call by value and call by name, and for each reduction strategy we consider a type-and-effect system a la Danvy and Filinski as well as a system with a fixed answer type. The call-by-value type-and-effect system we present is a refinement of Danvy and Filinski's original type system, whereas the call-by-name type-and-effect system is new. From the normalization proofs, we extract call-by-value and call-by-name evaluators in continuation-passing style with two layers of continuations; by construction, these evaluators are instances of normalization by evaluation.

References

1. Zena M. Ariola, Hugo Herbelin, and Amr Sabry. A type-theoretic foundation of delimited continuations. Higher-Order and Symbolic Computation, 20(4):403--429, 2007.
2. Kenichi Asai. Online partial evaluation for shift and reset. In Peter Thiemann, editor, Proceedings of the 2002 ACM SIGPLAN Workshop on Partial Evaluation and Semantics--Based Program Manipulation (PEPM 2002), SIGPLAN Notices, Vol. 37, No 3, pages 19--30, Portland, Oregon, March 2002. ACM Press.
3. Kenichi Asai. Offline partial evaluation for shift and reset. In Nevin Heintze and Peter Sestoft, editors, Proceedings of the 2004 ACM SIGPLAN Symposium on Partial Evaluation and Semantics--Based Program Manipulation (PEPM 2004), pages 3--14, Verona, Italy, August 2003. ACM Press.
4. Kenichi Asai. Logical relations for call-by-value delimited continuations. In Marko van Eekelen, editor, Proceedings of the Sixth Symposium on Trends in Functional Programming (TFP 2005), pages 413--428, Tallinn, Estonia, September 2005. Institute of Cybernetics at Tallinn Technical University. Extended version available as Technical Report of Department of Information Science, Ochanomizu University, OCHA-IS 06-1.
5. Kenichi Asai and Yukiyoshi Kameyama. Polymorphic delimited continuations. In Proceedings of the Fifth Asian symposium on Programming Languages and Systems, APLAS'07, number 4807 in Lecture Notes in Computer Science, pages 239--254, Singapore, December 2007.
6. Ulrich Berger. Program extraction from normalization proofs. In Marc Bezem and Jan Friso Groote, editors, Typed Lambda Calculi and Applications, number 664 in Lecture Notes in Computer Science, pages 91--106, Utrecht, The Netherlands, March 1993. Springer-Verlag.
7. Ulrich Berger, Stefan Berghofer, Pierre Letouzey, and Helmut Schwichtenberg. Program extraction from normalization proofs. Studia Logica, 82(1):25--49, 2006.
8. Ulrich Berger and Helmut Schwichtenberg. An inverse of the evaluation functional for typed lambda calculus. In Gilles Kahn, editor, Proceedings of the Sixth Annual {IEEE} Symposium on Logic in Computer Science, pages 203--211, Amsterdam, The Netherlands, July 1991. IEEE Computer Society Press.
9. Malgorzata Biernacka and Dariusz Biernacki. A context-based approach to proving termination of evaluation. In Proceedings of the 25th Annual Conference on Mathematical Foundations of Programming Semantics(MFPS XXV), Oxford, UK, April 2009.
10. Malgorzata Biernacka, Dariusz Biernacki, and Olivier Danvy. An operational foundation for delimited continuations in the CPS hierarchy. Logical Methods in Computer Science, 1(2:5):1--39, November 2005. A preliminary version was presented at the Fourth ACM SIGPLAN Workshop on Continuations (CW'04).
11. Malgorzata Biernacka, Olivier Danvy, and Kristian Stovring. Program extraction from proofs of weak head normalization. In Martin Escardo, Achim Jung, and Michael Mislove, editors, Proceedings of the 21st Annual Conference on Mathematical Foundations of Programming Semantics(MFPS XXI), volume 155 of Electronic Notes in Theoretical Computer Science, pages 169--189, Birmingham, UK, May 2005. Elsevier Science Publishers. Extended version available as the research report BRICS RS-05-12.
12. Dariusz Biernacki and Olivier Danvy. From interpreter to logic engine by defunctionalization. In Maurice Bruynooghe, editor, Logic Based Program Synthesis and Transformation, 13th International Symposium, LOPSTR 2003, number 3018 in Lecture Notes in Computer Science, pages 143--159, Uppsala, Sweden, August 2003. Springer-Verlag.
13. Dariusz Biernacki, Olivier Danvy, and Chung-chieh Shan. On the static and dynamic extents of delimited continuations. Science of Computer Programming, 60(3):274--297, 2006.
14. Thierry Coquand and Peter Dybjer. Intuitionistic model constructions and normalization proofs. Mathematical Structures in Computer Science, 7:75--94, 1997.
15. Olivier Danvy. Type-directed partial evaluation. In Guy L. Steele Jr., editor, Proceedings of the Twenty-Third Annual ACM Symposium on Principles of Programming Languages, pages 242--257, St. Petersburg Beach, Florida, January 1996. ACM Press.
16. Olivier Danvy. On evaluation contexts, continuations, and the rest of the computation. In Hayo Thielecke, editor, Proceedings of the Fourth ACM SIGPLAN Workshop on Continuations (CW'04), Technical report CSR-04-1, Department of Computer Science, Queen Mary's College, pages 13--23, Venice, Italy, January 2004.
17. Olivier Danvy. Defunctionalized interpreters for programming languages. In Peter Thiemann, editor, Proceedings of the 2008 ACM SIGPLAN International Conference on Functional Programming (ICFP'08), SIGPLAN Notices, Vol. 43, No. 9, Victoria, British Columbia, September 2008. ACM Press. Invited talk.
18. Olivier Danvy and Andrzej Filinski. A functional abstraction of typed contexts. DIKU Rapport 89/12, DIKU, Computer Science Department, University of Copenhagen, Copenhagen, Denmark, July 1989.
19. Olivier Danvy and Andrzej Filinski. Abstracting control. In Mitchell Wand, editor, Proceedings of the 1990 ACM Conference on Lisp and Functional Programming, pages 151--160, Nice, France, June 1990. ACM Press.
20. Olivier Danvy and Andrzej Filinski. Representing control, a study of the CPS transformation. Mathematical Structures in Computer Science, 2(4):361--391, 1992.
21. Peter Dybjer and Andrzej Filinski. Normalization and partial evaluation. In Gilles Barthe, Peter Dybjer, Luis Pinto, and Joao Saraiva, editors, Applied Semantics -- Advanced Lectures, number 2395 in Lecture Notes in Computer Science, pages 137--192, Caminha, Portugal, September 2000. Springer-Verlag.
22. Matthias Felleisen. The Calculi of lambda-v-CS Conversion: A Syntactic Theory of Control and State in Imperative Higher-Order Programming Languages. PhD thesis, Computer Science Department, Indiana University, Bloomington, Indiana, August 1987.
23. Matthias Felleisen and Daniel P. Friedman. Control operators, the SECD machine, and the lambda calculus. In Martin Wirsing, editor, Formal Description of Programming Concepts III, pages 193--217. Elsevier Science Publishers B.V. (North-Holland), Amsterdam, 1986.
24. Andrzej Filinski. Representing monads. In Hans-J. Boehm, editor, Proceedings of the Twenty-First Annual ACM Symposium on Principles of Programming Languages, pages 446--457, Portland, Oregon, January 1994. ACM Press.
25. Andrzej Filinski. Representing layered monads. In Alex Aiken, editor, Proceedings of the Twenty-Sixth Annual ACM Symposium on Principles of Programming Languages, pages 175--188, San Antonio, Texas, January 1999. ACM Press.
26. Robert Harper, Bruce F. Duba, and David MacQueen. Typing first-class continuations in ML. Journal of Functional Programming, 3(4):465--484, October 1993. A preliminary version was presented at the Eighteenth Annual ACM Symposium on Principles of Programming Languages (POPL 1991).
27. Hugo Herbelin and Silvia Ghilezan. An approach to call-by-name delimited continuations. In Philip Wadler, editor, Proceedings of the Thirty-Fifth Annual ACM Symposium on Principles of Programming Languages, pages 383--394. ACM Press, January 2008.
28. Yukiyoshi Kameyama. Axioms for delimited continuations in the CPS hierarchy. In Jerzy Marcinkowski and Andrzej Tarlecki, editors, Computer Science Logic, 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL, Proceedings, volume 3210 of Lecture Notes in Computer Science, pages 442--457, Karpacz, Poland, September 2004. Springer.
29. Yukiyoshi Kameyama and Kenichi Asai. Strong normalization of polymorphic calculus for delimited continuations. In Proceedings of the Austrian--Japanese Workshop on Symbolic Computation in Software Science (SCSS 2008), RISC-Linz Report Series No. 08-08, pages 96--108, Hagenberg, Austria, July 2008.
30. Yukiyoshi Kameyama and Masahito Hasegawa. A sound and complete axiomatization of delimited continuations. In Olin Shivers, editor, Proceedings of the 2003 ACM SIGPLAN International Conference on Functional Programming (ICFP'03), SIGPLAN Notices, Vol. 38, No. 9, pages 177--188, Uppsala, Sweden, August 2003. ACM Press.
31. Oleg Kiselyov. Call-by-name linguistic side effects. In Proceedings of the 2008 Workshop on Symmetric calculi and Ludics for the semantic interpretation, Hamburg, Germany, August 2008.
32. Oleg Kiselyov, Chung-chieh Shan, Daniel P. Friedman, and Amr Sabry. Backtracking, interleaving, and terminating monad transformers. In Benjamin Pierce, editor, Proceedings of the 2005 ACM SIGPLAN International Conference on Functional Programming (ICFP'05), SIGPLAN Notices, Vol. 40, No. 9, pages 192--203, Tallinn, Estonia, September 2005. ACM Press.
33. Chethan R. Murthy. Control operators, hierarchies, and pseudo-classical type systems: A-translation at work. In Olivier Danvy and Carolyn L. Talcott, editors, Proceedings of the First ACM SIGPLAN Workshop on Continuations (CW'92), Technical report STAN-CS-92-1426, Stanford University, pages 49--72, San Francisco, California, June 1992.
34. Gordon D. Plotkin. Call-by-name, call-by-value and the lambda calculus. Theoretical Computer Science, 1:125--159, 1975.
35. Chung-chieh Shan. Delimited continuations in natural language: quantification and polarity sensitivity. In Hayo Thielecke, editor, Proceedings of the Fourth ACM SIGPLAN Workshop on Continuations (CW'04), Technical report CSR-04-1, Department of Computer Science, Queen Mary's College, pages 55--64, Venice, Italy, January 2004.
36. Eijiro Sumii. An implementation of transparent migration on standard Scheme. In Matthias Felleisen, editor, Proceedings of the Workshop on Scheme and Functional Programming, Technical Report 00-368, Rice University, pages 61--64, Montreal, Canada, September 2000.
37. William W. Tait. Intensional interpretation of functionals of finite type I. Journal of Symbolic Logic, 32:198--212, 1967.
38. Hayo Thielecke, editor. Proceedings of the Fourth ACM SIGPLAN Workshop on Continuations (CW'04), Technical report CSR-04-1, Department of Computer Science, Queen Mary's College, Venice, Italy, January 2004.
39. Peter Thiemann. Combinators for program generation. Journal of Functional Programming, 9(5):483--525, 1999.
40. Anne S. Troelstra, editor. Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, volume 344 of Lecture Notes in Mathematics. Springer-Verlag, 1973.

Index Terms

• Software and its engineering

  • Software notations and tools

    • General programming languages

      • Language features

        • Control structures

• Theory of computation

  • Semantics and reasoning

    • Program semantics

      • Operational semantics