{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:12:08Z","timestamp":1775790728041,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540417392","type":"print"},{"value":"9783540447160","type":"electronic"}],"license":[{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44716-4_4","type":"book-chapter","created":{"date-parts":[[2007,8,15]],"date-time":"2007-08-15T18:16:34Z","timestamp":1187201794000},"page":"61-77","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Proving Syntactic Properties of Exceptions in an Ordered Logical Framework"],"prefix":"10.1007","author":[{"given":"Jeff","family":"Polakow","sequence":"first","affiliation":[]},{"given":"Kwangkeun","family":"Yi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,3,21]]},"reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"Andrew W. Appel. Modern Compiler Implementation in ML\/C\/Java: Basic Techniques. Cambridge University Press, 1997.","DOI":"10.1017\/CBO9780511811449"},{"key":"4_CR2","unstructured":"Josh Berdine, Peter O\u2019Hearn, Uday S. Reddy, and Hayo Thielecke. Linearly used continuations. In Informal Proceedings of The Third ACM SIGPLAN Workshop on Continuations (CW \u201901), January 2001. To appear."},{"key":"4_CR3","unstructured":"Iliano Cervesato and Frank Pfenning. A linear logical framework. Information and Computation, 1999. To appear in the special issue with invited papers from LICS\u201996, E. Clarke, editor."},{"key":"4_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"88","DOI":"10.1007\/3-540-46425-5_6","volume-title":"Formalizing implementation strategies for first-class continuations","author":"O. Danvy","year":"2000","unstructured":"Olivier Danvy. Formalizing implementation strategies for first-class continuations. In Programming Languages and Systems, The Proceedings of the 9th European Symposium On Programming, volume 1782 of Lecture Notes in Computer Science, pages 88\u2013103, 2000."},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"]Olivier Danvy, Belmina Dzac, and Frank Pfenning. On proving syntactic properties of cps programs. In Third International Workshop on Higher Order Operational Techniques in Semantics (HOOTS\u201999), Paris, France, September 1999.","DOI":"10.7146\/brics.v6i23.20092"},{"issue":"4","key":"4_CR6","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1017\/S0960129500001535","volume":"2","author":"O. Danvy","year":"1992","unstructured":"Olivier Danvy and Andrzej Filinski. Representing control: a study of the CPS transformation. Mathematical Structures in Computer Science, 2(4):361\u2013391, December 1992.","journal-title":"Mathematical Structures in Computer Science"},{"key":"4_CR7","volume-title":"Technical Report CMU-CS-95-121","author":"O. Danvy","year":"1995","unstructured":"Olivier Danvy and Frank Pfenning. The occurrence of continuation parameters in CPS terms. Technical Report CMU-CS-95-121, Department of Computer Science, Carnegie Mellon University, February 1995."},{"key":"4_CR8","series-title":"PhD thesis","volume-title":"The Calculi of \u03bb-v-CS Conversion: A Syntactic Theory of Control and State in Imperative Higher-Order Programming Languages","author":"M. Felleisen","year":"1987","unstructured":"Matthias Felleisen. The Calculi of \u03bb-v-CS Conversion: A Syntactic Theory of Control and State in Imperative Higher-Order Programming Languages. PhD thesis, Department of Computer Science, Indiana University, Bloomington, Indiana, August 1987."},{"issue":"3","key":"4_CR9","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1017\/S0956796897002748","volume":"7","author":"J. Hatcliff","year":"1997","unstructured":"John Hatcliff and Olivier Danvy. Thunks and the \u03bb-calculus. Journal of Functional Programming, 7(3):303\u2013320, 1997.","journal-title":"Journal of Functional Programming"},{"issue":"1","key":"4_CR10","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R. Harper","year":"1993","unstructured":"Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the Association for Computing Machinery, 40(1):143\u2013184, January 1993.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"4_CR11","unstructured":"Jungtaek Kim, Kwangkeun Yi, and Olivier Danvy. Assessing the overhead of ml exceptions by selective cps transformation. In The Proceedings of the ACM SIGPLAN Workshop on ML, pages 103\u2013114, September 1998."},{"key":"4_CR12","series-title":"Lect Notes Comput Sci","first-page":"119","volume-title":"The practice of logical frameworks","author":"F. Pfenning","year":"1986","unstructured":"Frank Pfenning. The practice of logical frameworks. In H\u00e9l\u00e8ne Kirchner, editor, Proceedings of the Colloquium on Trees in Algebra and Programming, pages 119\u2013134, Link\u00f6ping, Sweden, April 1996. Springer-Verlag LNCS 1059. Invited talk."},{"key":"4_CR13","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/0304-3975(75)90017-1","volume":"1","author":"G. D. Plotkin","year":"1975","unstructured":"Gordon D. Plotkin. Call-by-name, call-by-value and the \u03bb-calculus. Theoretical Computer Science, 1:125\u2013159, 1975.","journal-title":"Theoretical Computer Science"},{"key":"4_CR14","unstructured":"Gordon D. Plotkin. A structural approach to operational semantics. Technical report, Aarhus University, September 1981."},{"key":"4_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1007\/3-540-48959-2_21","volume-title":"Natural deduction for intuitionistic non-commutative linear logic","author":"J. Polakow","year":"1999","unstructured":"Jeff Polakow and Frank Pfenning. Natural deduction for intuitionistic non-commutative linear logic. In J.-Y. Girard, editor, Proceedings of the Fourth International Conference on Typed Lambda Calculi and Applications (TLCA\u201999), pages 295\u2013309, l\u2019Aquila, Italy, April 1999. Springer-Verlag LNCS 1581."},{"key":"4_CR16","doi-asserted-by":"crossref","unstructured":"Jeff Polakow and Frank Pfenning. Relating natural deduction and sequent calculus for intuitionistic non-commutative linear logic. In Andre Scedrov and Achim Jung, editors, Proceedings of the 15th Conference on Mathematical Foundations of Programming Semantics, pages 311\u2013328, New Orleans, Louisiana, April 1999. Electronic Notes in Theoretical Computer Science, Volume 20.","DOI":"10.1016\/S1571-0661(04)80088-4"},{"key":"4_CR17","unstructured":"Jeff Polakow and Frank Pfenning. Properties of terms in continuation passing style in an ordered logical framework. In Workshop on Logical Frameworks and Meta-Languages (LFM 2000), Santa Barbara, California, June 2000."},{"key":"4_CR18","series-title":"Technical Report","volume-title":"A compiler for Scheme","author":"G. L. Steele Jr","year":"1978","unstructured":"Guy L. Steele Jr. Rabbit: A compiler for Scheme. Technical Report AI-TR-474, Artificial Intelligence Laboratory, Massachusetts Institute of Technology, Cambridge, Massachusetts, May 1978."}],"container-title":["Lecture Notes in Computer Science","Functional and Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44716-4_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,2,8]],"date-time":"2021-02-08T22:14:20Z","timestamp":1612822460000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44716-4_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540417392","9783540447160"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-44716-4_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2001]]},"assertion":[{"value":"21 March 2001","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}