|
 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
Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.
| |
1
|
|
 |
2
|
|
| |
3
|
|
| |
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
|
|
| |
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
|
|
| |
14
|
|
| |
15
|
|
| |
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
|
|
| |
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
|
|
| |
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 , Andrzej Filinski, Normalization and Partial Evaluation, Applied Semantics, International Summer School, APPSEM 2000, Caminha, Portugal, September 9-15, 2000, Advanced Lectures, p.137-192, September 09-15, 2000
|
| |
22
|
|
| |
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
|
|
| |
25
|
|
| |
26
|
Bruce Duba , Robert Harper , David MacQueen, Typing first-class continuations in ML, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.163-173, January 21-23, 1991, Orlando, Florida, United States
[doi> 10.1145/99583.99608]
|
| |
27
|
|
| |
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
|
|
| |
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 , Amr Sabry, Backtracking, interleaving, and terminating monad transformers: (functional pearl), Proceedings of the tenth ACM SIGPLAN international conference on Functional programming, September 26-28, 2005, Tallinn, Estonia
|
| |
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
|
|
| |
40
|
Anne S. Troelstra, editor. Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, volume 344 of Lecture Notes in Mathematics. Springer-Verlag, 1973.
|
|
Adobe Acrobat
QuickTime
Windows Media Player
Real Player
Pdf
D.3