An approach to call-by-name delimited continuations. (English) Zbl 1295.68063
Proceedings of the 35th ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’08, San Francisco, CA, USA, January 07–12, 2008. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-59593-689-9). 383-394 (2008).
MSC:
| 68N18 | Functional programming and lambda calculus |
| 03B70 | Logic in computer science |
| 68N15 | Theory of programming languages |
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
Citations:
Zbl 1213.68187References:
| [1] | Zena M. Ariola and Hugo Herbelin. Control reduction theories: the benefit of structural substitution. J. Funct. Program., 2007. Includes a Historical Note by Matthias Felleisen. To appear. 10.1017/S0956796807006612 · Zbl 1138.68020 |
| [2] | Zena M. Ariola, Hugo Herbelin, and Amr Sabry. A type-theoretic foundation of delimited continuations. Higher Order and Symbolic Computation, 2007. To appear. 10.1007/s10990-007-9006-0 · Zbl 1213.68187 |
| [3] | Kensuke Baba, Sachio Hirokawa, and Ken-etsu Fujita. Parallel reduction in type free λμ-calculus. Electronic Notes in Theoretical Computer Science, 42: 52-66, 2001. |
| [4] | Malgorzata Biernacka, Dariusz Biernacki, and Olivier Danvy. An operational foundation for delimited continuations. Technical Report 03-41, BRICS, University of Aarhus, Denmark, 2003. |
| [5] | Dariusz Biernacki and Olivier Danvy. On the dynamic extent of delimited continuations. Technical Report 05-2, BRICS, University of Aarhus, Denmark, 2005. · Zbl 1191.68157 |
| [6] | Pierre-Louis Curien and Hugo Herbelin. The duality of computation. In Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming, ICFP 2000, Montreal, Canada, September 18-21, 2000, SIGPLAN Notices 35(9), pages 233-243. ACM, 2000. ISBN 1-58113-202-6. 10.1145/351240.351262 · Zbl 1321.68146 |
| [7] | Vincent Danos, Hugo Herbelin, and Laurent Regnier. Game semantics & abstract machines. In Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science (LICS ’96), pages 394-405. IEEE Computer Society Press, 1996. |
| [8] | Olivier Danvy and Andrzej Filinski. A functional abstraction of typed contexts. Technical Report 89/12, DIKU, University of Copenhagen, Copenhagen, Denmark, August 1989. |
| [9] | René David and Walter Py. λμ-calculus and Böhm’s theorem. J. Symb. Log., 66(1):407-413, 2001. · Zbl 0981.03019 |
| [10] | Philippe de Groote. A CPS-translation of the λμ-calculus. In STison, editor, Proceedings of the Colloquium on Trees in Algebra and Programming, CAAP’94, Edinburgh, U.K., April 11-13, 1994, volume 787 of Lecture Notes in Computer Science, pages 85-99. Springer-Verlag, 1994. ISBN 3-540-57879-X. · Zbl 0938.03024 |
| [11] | Kosta Došen and Zoran Petrić. The typed Böhm teorem. In Böhm theorem: applications to Computer Science Theory – BOTH 2001 Crete, Greece, volume 50(2) of Electronic Notes in Theoretical Computer Science, page 13, 2001. |
| [12] | Matthias Felleisen. The theory and practice of first-class prompts. In Proceedings of the 15th ACM Symposium on Principles of Programming Languages (POPL ’88), pages 180-190. ACM Press, New York, January 1988. 10.1145/73560.73576 |
| [13] | Matthias Felleisen and Daniel Friedman. Control operators, the secd machine, and the λ-calculus. In Formal description of programming concepts-III, pages 193-217. North-Holland, 1986. |
| [14] | Matthias Felleisen, Daniel P. Friedman, Eugene Kohlbecker, and Bruce F. Duba. Reasoning with continuations. In First Symposium on Logic and Computer Science, pages 131-141, 1986. |
| [15] | Andrzej Filinski. Representing monads. In Conf. Record 21st ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, POPL’94, Portland, OR, USA, 17-21 Jan. 1994, pages 446-457. ACM Press, New York, 1994. 10.1145/174675.178047 |
| [16] | Michael J. Fischer. λ-calculus schemata. In Proc. ACM Conference on Proving Assertions About Programs, volume 7(1) of SIGPLAN Notices, pages 104-109. ACM Press, New York, 1972. 10.1145/942578.807077 |
| [17] | Ken-etsu Fujita. A sound and complete cps-translation for λμ-calculus. In TLCA, pages 120-134, 2003. · Zbl 1040.03008 |
| [18] | Timothy G. Griffin. The formulae-as-types notion of control. In Conf. Record 17th Annual ACM Symp. on Principles of Programming Languages, POPL ’90, San Francisco, CA, USA, 17-19 Jan 1990, pages 47-57. ACM Press, New York, 1990. 10.1145/96709.96714 |
| [19] | Thèrése Hardin, Luc Maranget, and Bruno Pagano. Functional back-ends within the lambda-sigma calculus. In ICFP, pages 25-33, 1996. 10.1145/232627.232632 · Zbl 1345.68056 |
| [20] | Hugo Herbelin. Explicit substitutions and reducibility. Journal of Logic and Computation, 11(3): 431-451, 2001. · Zbl 0984.03014 |
| [21] | Hugo Herbelin. C’est maintenant qu’on calcule: au cæ ur de la dualité. Habilitation à diriger les recherches, Université Paris 11, December 2005. |
| [22] | Hugo Herbelin. Séquents qu’on calcule: de l’interprétation du calcul des séquents comme calcul de λ-termes et comme calcul de stratégies gagnantes. Thése de doctorat, Université Paris 7, January 1995. |
| [23] | Hugo Herbelin. Games and weak-head reduction for classical PCF. In Philippe de Groote and JRoger Hindley, editors, Third International Conference on Typed Lambda Calculi and Applications, TLCA ’97, Nancy, France, April 2-4, 1997, Proceedings, volume 1210 of Lecture Notes in Computer Science, pages 214-230. Springer, 1997. ISBN 3-540-62688-3. · Zbl 1063.68563 |
| [24] | Gregory F. Johnson. Gl – a denotational testbed with continuations and partial continuations as first-class objects. In SIGPLAN ’87: Papers of the Symposium on Interpreters and interpretive techniques, pages 165-176, New York, NY, USA, 1987. ACM Press. ISBN 0-89791-235-7. http://doi.acm.org/10.1145/29650.29668. 10.1145/29650.29668 |
| [25] | Gregory F. Johnson and Dominic Duggan. Stores and partial continuations as first-class objects in a language and its environment. In POPL, pages 158-168, 1988. 10.1145/73560.73574 |
| [26] | Thierry Joly. Codages, séparabilité et représentation de fonctions dans divers λ-calculs typés. Phd thesis, Université Paris 7, January 2000. |
| [27] | Yukiyoshi Kameyama and Masahito Hasegawa. A sound and complete axiomatization of delimited continuations. In Colin Runciman and Olin Shivers, editors, Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, ICFP 2003, Uppsala, Sweden, August 25-29, 2003, volume 38(9) of SIGPLAN Notices, pages 177-188. ACM Press, New York, 2003. 10.1145/944705.944722 · Zbl 1315.68098 |
| [28] | Yves Lafont, Bernhard Reus, and Thomas Streicher. Continuations semantics or expressing implication by negation. Technical Report 9321, Ludwig-Maximilians-Universität, München, 1993. |
| [29] | C.-H. Luke Ong. A semantic view of classical proofs: type-theoretic, categorical, denotational characterizations. In Proceedings of 11th IEEE Annual Symposium on Logic in Computer Science, pages 230-241. IEEE Computer Society Press, 1996. |
| [30] | C.-H. Luke Ong and Charles A. Stewart. A Curry-Howard foundation for functional computation with control. In Proceedings of ACM SIGPLAN-SIGACT Symposium on Principle of Programming Languages, Paris, January 1997, pages 215-227. ACM Press, 1997. 10.1145/263699.263722 |
| [31] | Luca Paolini. Call-by-Value separability and computability. In ARestivo and SRonchi della Rocca, editors, 7th Italian Conference Theoretical Computer Science, ICTCS’05, volume 2202 of Lecture Notes in Computer Science, pages 74-89. Springer-Verlag, 2001. · Zbl 1042.68030 |
| [32] | Michel Parigot. Lambda-mu-calculus: An algorithmic interpretation of classical natural deduction. In Logic Programming and Automated Reasoning: International Conference LPAR ’92 Proceedings, St. Petersburg, Russia, pages 190-201. Springer-Verlag, 1992. · Zbl 0925.03092 |
| [33] | David Pym and Eike Ritter. On the semantics of classical disjunction. Journal of Pure and Applied Algebra, 159:315-338, 2001. · Zbl 0981.03018 |
| [34] | Amr Sabry. Note on axiomatizing the semantics of control operators. Technical Report CIS-TR-96-03, Dept of Information Science, Univ. of Oregon, 1996. |
| [35] | Amr Sabry and Matthias Felleisen. Reasoning about programs in continuation-passing style. Lisp and Symbolic Computation, 6(3-4): 289-360, 1993. 10.1007/BF01019462 |
| [36] | Alexis Saurin. Separation with streams in the λμ-calculus. In Proceedings, 20th Annual IEEE Symposium on Logic in Computer Science (LICS ’05), pages 356-365. IEEE Computer Society Press, 2005. 10.1109/LICS.2005.48 |
| [37] | Alexis Saurin. Typing streams in the λμ-calculus. In 14th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR ’07), Lecture Notes in Artificial Intelligence. Springer-Verlag, 2007. to appear. |
| [38] | Peter Selinger. Control categories and duality: on the categorical semantics of the λμ-calculus. Mathematical Structures in Computer Science, 11 (2):207-260, 2001. 10.1017/S096012950000311X · Zbl 0984.18003 |
| [39] | Chung-chieh Shan. Shift to control. In Olin Shivers and Oscar Waddell, editors, Proceedings of the 5th workshop on Scheme and Functional Programming, pages 99-107, 2004. |
| [40] | Alex K. Simpson. Categorical completeness results for simply typed lambda calculus. In MDezani-Ciancaglini and GPlotkin, editors, Typed Lambda Calculus and Applications TLCA’95, volume 902 of Lecture Notes in Computer Science, pages 414-427. Springer-Verlag, 1995. · Zbl 1063.03524 |
| [41] | Dorai Sitaram and Matthias Felleisen. Reasoning with continuations ii: full abstraction for models of control. In LFP ’90: Proceedings of the 1990 ACM conference on LISP and functional programming, pages 161-175. ACM Press, 1990. ISBN 0-89791-368-X. http://doi.acm.org/10.1145/91556.91626. 10.1145/91556.91626 |
| [42] | Richard Statman. Completeness, invariance and λ-definability. J. Symb. Log., 47(1):17-26, 1982. · Zbl 0487.03006 |
| [43] | Philip Wadler. Call-by-value is dual to call-by-name. In Colin Runciman and Olin Shivers, editors, Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, ICFP 2003, Uppsala, Sweden, August 25-29, 2003, volume 38(9) of SIGPLAN Notices, pages 189-201. ACM, 2003. ISBN 1-58113-756-7. 10.1145/944705.944723 · Zbl 1315.68060 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
