{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:43:35Z","timestamp":1780994615374,"version":"3.54.1"},"reference-count":42,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2008,11,7]],"date-time":"2008-11-07T00:00:00Z","timestamp":1226016000000},"content-version":"unspecified","delay-in-days":5516,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[1993,10]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>An extension of ML with continuation primitives similar to those found in Scheme is considered. A number of alternative type systems are discussed, and several programming examples are given. A continuation-based operational semantics is defined for a small, purely functional language, and the soundness of the Damas\u2013Milner polymorphic type assignment system with respect to this semantics is proved. The full Damas\u2013Milner type system is shown to be unsound in the presence of first-class continuations. Restrictions on polymorphism similar to those introduced in connection with reference types are shown to suffice for soundness.<\/jats:p>","DOI":"10.1017\/s095679680000085x","type":"journal-article","created":{"date-parts":[[2008,11,7]],"date-time":"2008-11-07T11:13:12Z","timestamp":1226056392000},"page":"465-484","source":"Crossref","is-referenced-by-count":33,"title":["Typing first-class continuations in ML"],"prefix":"10.1017","volume":"3","author":[{"given":"Robert","family":"Harper","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Bruce F.","family":"Duba","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"David","family":"Macqueen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2008,11,7]]},"reference":[{"key":"S095679680000085X_ref042","author":"Wright","year":"1991"},{"key":"S095679680000085X_ref040","doi-asserted-by":"crossref","unstructured":"Wand M. (1980) Continuation-based multiprocessing. In Conference Record of the 1980 LISP Conference, pp. 19\u201328.","DOI":"10.1145\/800087.802786"},{"key":"S095679680000085X_ref039","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(90)90018-D"},{"key":"S095679680000085X_ref038","unstructured":"Tofte M. (1988) Operational Semantics and Polymorphic Type Inference. PhD thesis, Edinburgh University, 1988. Available as Edinburgh University Laboratory for Foundations of Computer Science Technical Report ECS-LFCS-88-54."},{"key":"S095679680000085X_ref036","author":"Sussman","year":"1975"},{"key":"S095679680000085X_ref033","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(85)80001-2"},{"key":"S095679680000085X_ref031","first-page":"717","volume-title":"Conference Record of the 25th National ACM Conference","author":"Reynolds","year":"1972"},{"key":"S095679680000085X_ref030","doi-asserted-by":"publisher","DOI":"10.1145\/362349.362364"},{"key":"S095679680000085X_ref029","unstructured":"Reppy J. (1990) Asynchronous signals in Standard ML (unpublished manuscript), 08."},{"key":"S095679680000085X_ref024","first-page":"219","volume-title":"Lecture Notes in Computer Science","volume":"224","author":"Meyer","year":"1985"},{"key":"S095679680000085X_ref023","doi-asserted-by":"publisher","DOI":"10.1145\/363744.363749"},{"key":"S095679680000085X_ref022","doi-asserted-by":"publisher","DOI":"10.1016\/0096-0551(86)90007-X"},{"key":"S095679680000085X_ref020","doi-asserted-by":"publisher","DOI":"10.1016\/0096-0551(87)90003-8"},{"key":"S095679680000085X_ref019","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(87)90016-1"},{"key":"S095679680000085X_ref008","unstructured":"Felleisen M. (1985) Transliterating Prolog into Scheme. Technical Report 182, Indiana University Computer Science Department."},{"key":"S095679680000085X_ref001","first-page":"1","volume-title":"Third International Symposium on Programming Language Implementation and Logic Programming","author":"Appel","year":"1991"},{"key":"S095679680000085X_ref006","doi-asserted-by":"publisher","DOI":"10.1016\/0096-0551(89)90018-0"},{"key":"S095679680000085X_ref032","unstructured":"Sitaram D. and Felleisen M. (1990) Reasoning with continuations. II. Full abstraction for models of control. In Proc. 1990 Conference on LISP and Functional Programming. pp. 161\u2013175, 06."},{"key":"S095679680000085X_ref010","volume-title":"Formal Description of Programming Concepts III","author":"Felleisen","year":"1986"},{"key":"S095679680000085X_ref041","unstructured":"Wright A. and Felleisen M. (1990) The nature of exceptions in polymorphic languages. Unpublished manuscript, Rice University."},{"key":"S095679680000085X_ref003","unstructured":"Cooper E. C. and Morrisett J. G. (1990) Adding threads to Standard ML. Technical Report CMU-CS-90-186, School of Computer Science, Carnegie Mellon University."},{"key":"S095679680000085X_ref026","first-page":"363","volume-title":"To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus and Formalism","author":"Plotkin","year":"1980"},{"key":"S095679680000085X_ref016","volume-title":"Seventeenth ACM Symposium on Principles of Programming Languages","author":"Griffin","year":"1990"},{"key":"S095679680000085X_ref037","volume-title":"Proc. 1987 Workshop of Foundations of Logic and Functional Programming","volume":"306","author":"Talcott","year":"1988"},{"key":"S095679680000085X_ref015","first-page":"263","volume-title":"Program Transformations and Programming Environments","author":"Friedman","year":"1985"},{"key":"S095679680000085X_ref034","author":"Strachey","year":"1974"},{"key":"S095679680000085X_ref035","unstructured":"Sufrin B. (1979) CSP-style processes in ML (private communication)."},{"key":"S095679680000085X_ref028","unstructured":"Reppy J. (1989) First-class synchronous operations in standard ML. Technical Report TR 89\u20131068, Computer Science Department, Cornell University, Ithaca, NY, December."},{"key":"S095679680000085X_ref018","first-page":"13","volume-title":"Proceedings of the ACM SIGPLAN Work-shop on Continuations CW92","author":"Harper","year":"1992"},{"key":"S095679680000085X_ref025","volume-title":"The Definition of Standard ML","author":"Milner","year":"1990"},{"key":"S095679680000085X_ref027","unstructured":"Ramsey N. (1990) Concurrent programming in ML. Technical Report CS-TR-262-90, Computer Science Department, Princeton University."},{"key":"S095679680000085X_ref021","doi-asserted-by":"publisher","DOI":"10.1145\/29873.30392"},{"key":"S095679680000085X_ref014","unstructured":"Filinski A. (1989) Declarative continuations and categorical duality. Master's thesis. University of Copenhagen, Denmark, 08. (DIKU Report 89\/11.)"},{"key":"S095679680000085X_ref005","doi-asserted-by":"crossref","unstructured":"Duba B. , Harper R. and MacQueen D. (1991) Typing first-class continuations in ML. In Eighteenth ACM Symposium on Principles of Programming Languages, January.","DOI":"10.1145\/99583.99608"},{"key":"S095679680000085X_ref002","first-page":"237","volume-title":"Algebraic Methods in Semantics","author":"Clinger","year":"1985"},{"key":"S095679680000085X_ref004","first-page":"207","volume-title":"Ninth ACM Symposium on Principles of Programming Languages","author":"Damas","year":"1982"},{"key":"S095679680000085X_ref007","doi-asserted-by":"crossref","unstructured":"Evans A. (1968) PAL \u2013 a language designed for teaching programming linguistics. In Proc. ACM 23rd National Conference, pp. 395\u2013403, Princeton.ACM, Brandin Systems Press.","DOI":"10.1145\/800186.810604"},{"key":"S095679680000085X_ref009","doi-asserted-by":"crossref","unstructured":"Felleisen M. (1988) The theory and practice of first-class prompts. In Fifteenth ACM Symposium on Principles of Programming Languages, pp. 180\u2013190, San Diego, CA.ACM.","DOI":"10.1145\/73560.73576"},{"key":"S095679680000085X_ref011","volume-title":"First Symposium on Logic in Computer Science","author":"Felleisen","year":"1986"},{"key":"S095679680000085X_ref012","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90109-5"},{"key":"S095679680000085X_ref013","unstructured":"Filinski A. (1989) Declarative continuations: An investigation of duality in programming language semantics in Summer Conference on Category Theory and Computer Science, Manchester, UK, volume 389 of Lecture Notes in Computer Science. Springer-Verlag."},{"key":"S095679680000085X_ref017","unstructured":"Griffin G. T. (1992) Logical interpretations and computational simulations. Technical memoranda, AT&T Bell Laboratories, in preparation."}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S095679680000085X","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T22:35:12Z","timestamp":1779834912000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S095679680000085X\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993,10]]},"references-count":42,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1993,10]]}},"alternative-id":["S095679680000085X"],"URL":"https:\/\/doi.org\/10.1017\/s095679680000085x","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[1993,10]]}}}