{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:27:18Z","timestamp":1761611238046},"reference-count":42,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2008,11,7]],"date-time":"2008-11-07T00:00:00Z","timestamp":1226016000000},"content-version":"unspecified","delay-in-days":4573,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[1996,5]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We study the operational semantics of an extension of Girard's System F<jats:sub>\u03c9<\/jats:sub> with two control operators: an <jats:italic>abort<\/jats:italic> operation that abandons the current control context, and a <jats:italic>callcc<\/jats:italic> operation that captures the current control context. Two classes of operational semantics are considered, each with a call-by-value and a call-by-name variant, differing in their treatment of polymorphic abstraction and instantiation. Under the <jats:italic>standard<\/jats:italic> semantics, polymorphic abstractions are values and polymorphic instantiation is a significant computation step; under the <jats:italic>ML-like<\/jats:italic> semantics evaluation proceeds beneath polymorphic abstractions and polymorphic instantiation is computationally insignificant. Compositional, type-preserving continuation-passing style (cps) transformation algorithms are given for the standard semantics, resulting in terms on which all four evaluation strategies coincide. This has as a corollary the soundness and termination of well-typed programs under the standard evaluation strategies. In contrast, such results are obtained for the call-by-value ML-like strategy only for a restricted sub-language in which constructor abstractions are limited to values. The ML-like call-by-name semantics is indistinguishable from the standard call-by-name semantics when attention is limited to complete programs.<\/jats:p>","DOI":"10.1017\/s0956796800001775","type":"journal-article","created":{"date-parts":[[2008,11,7]],"date-time":"2008-11-07T11:10:59Z","timestamp":1226056259000},"page":"393-418","source":"Crossref","is-referenced-by-count":7,"title":["Operational interpretations of an extension of F<sub>\u03c9<\/sub> with control operators"],"prefix":"10.1017","volume":"6","author":[{"given":"Robert","family":"Harper","sequence":"first","affiliation":[]},{"given":"Mark","family":"Lillibridge","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2008,11,7]]},"reference":[{"key":"S0956796800001775_ref035","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90017-1"},{"key":"S0956796800001775_ref005","doi-asserted-by":"crossref","unstructured":"Cardelli L. , Martini S. , Mitchell J. C. and Scedrov A. (1991) An extension of System F with subtyping. Research Report 80, Digital Systems Research Center, Palo Alto, CA.","DOI":"10.1007\/3-540-54415-1_73"},{"key":"S0956796800001775_ref013","unstructured":"Girard J.-Y. (1972) Interpr\u00e9tation Fonctionnelle et \u00c9limination des Coupures dans I'Arithm\u00e9tique d'Ordre Sup\u00e9rieure. PhD thesis, Universit\u00e9 Paris VII."},{"key":"S0956796800001775_ref027","unstructured":"Leroy X. and Mauny M. (1992) The Caml Light system, version 0.5\u2014documentation and user's guide. Technical Report L-5, INRIA."},{"key":"S0956796800001775_ref026","doi-asserted-by":"crossref","unstructured":"Leroy X. (1992) Unboxed objects and polymorphic typing. Conference Record of the 19th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 177\u2013188, Albuquerque, NM.","DOI":"10.1145\/143165.143205"},{"key":"S0956796800001775_ref028","doi-asserted-by":"crossref","unstructured":"MacQueen D. (1986) Using dependent types to express modular structure. 13th ACM Symposium on Principles of Programming Languages.","DOI":"10.1145\/512644.512670"},{"key":"S0956796800001775_ref025","doi-asserted-by":"crossref","unstructured":"Kranz D. , Kelsey R. , Rees J. , Hudak P. , Philbin J. and Adams N. (1986) Orbit: An optimizing compiler for Scheme. Proc. SIGPLAN Symposium on Compiler Construction, pp. 219\u2013233.","DOI":"10.1145\/12276.13333"},{"key":"S0956796800001775_ref010","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90014-7"},{"key":"S0956796800001775_ref021","doi-asserted-by":"publisher","DOI":"10.1145\/169701.169696"},{"key":"S0956796800001775_ref019","first-page":"13","volume-title":"Proc. ACM SIGPLAN Workshop on Continuations CW92","author":"Harper","year":"1992"},{"key":"S0956796800001775_ref018","doi-asserted-by":"crossref","unstructured":"Harper R. and Lillibridge M. (1993) Explicit polymorphism and CPS conversion. 20th ACM Symposium on Principles of Programming Languages, pp. 206\u2013219, Charleston, SC.","DOI":"10.1145\/158511.158630"},{"key":"S0956796800001775_ref036","unstructured":"Reppy J. H. (1991) CML: A higher-order concurrent language. ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 293\u2013305."},{"key":"S0956796800001775_ref030","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"S0956796800001775_ref020","doi-asserted-by":"publisher","DOI":"10.1007\/BF01019463"},{"key":"S0956796800001775_ref041","volume-title":"RABBIT: A compiler for SCHEME","author":"Steele","year":"1978"},{"key":"S0956796800001775_ref012","unstructured":"Projet Formel .(1987) CAML: The reference manual. Technical report, INRIA\u2013ENS."},{"key":"S0956796800001775_ref032","volume-title":"The Definition of Standard ML","author":"Milner","year":"1990"},{"key":"S0956796800001775_ref014","volume-title":"Proofs and Types: Cambridge Tracts in Theoretical Computer Science","volume":"7","author":"Girard","year":"1989"},{"key":"S0956796800001775_ref022","doi-asserted-by":"publisher","DOI":"10.21236\/ADA290316"},{"key":"S0956796800001775_ref017","doi-asserted-by":"publisher","DOI":"10.1017\/S095679680000085X"},{"key":"S0956796800001775_ref008","doi-asserted-by":"crossref","unstructured":"Curien P.-L. and Ghelli G. (1990) Coherence of subsumption. Technical Report LIENS\u201390\u201310, Laboratoire d'Informatique de l'Ecole Normale Sup\u00e9rieure, Paris.","DOI":"10.1007\/3-540-52590-4_45"},{"key":"S0956796800001775_ref015","volume-title":"Edinburgh LCF: A Mechanized Logic of Computation: Lecture Notes in Computer Science 78","author":"Gordon","year":"1979"},{"key":"S0956796800001775_ref004","unstructured":"Cardelli L. (1989) Typeful programming. Technical Report 45, DEC Systems Research Center."},{"key":"S0956796800001775_ref033","doi-asserted-by":"crossref","unstructured":"Mitchell J. and Harper R. (1988) The essence of ML. 15th ACM Symposium on Principles of Programming Languages, San Diego, CA.","DOI":"10.1145\/73560.73563"},{"key":"S0956796800001775_ref042","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(90)90018-D"},{"key":"S0956796800001775_ref001","volume-title":"Compiling with Continuations","author":"Appel","year":"1992"},{"key":"S0956796800001775_ref031","volume-title":"Commentary on Standard ML","author":"Milner","year":"1991"},{"key":"S0956796800001775_ref002","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90055-7"},{"key":"S0956796800001775_ref003","doi-asserted-by":"crossref","unstructured":"Burstall R. , MacQueen D. and Sannella D. (1980) HOPE: An experimental applicative language. Proc. 1980 LISP Conference, pp. 136\u2013143, Stanford, CA.","DOI":"10.1145\/800087.802799"},{"key":"S0956796800001775_ref006","first-page":"1","article-title":"Revised4 Report on the Algorithmic Language Scheme","volume":"5","author":"Clinger","year":"1991","journal-title":"LISP Pointers"},{"key":"S0956796800001775_ref007","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":"S0956796800001775_ref034","doi-asserted-by":"crossref","unstructured":"Pierce B. C. (1993) Intersection types and bounded polymorphism. In: Bezem M. and Groote J. F. , editors, Proc. International Conference on Typed Lambda Calculi and Applications, TLCA'93, pp. 346\u2013360, Utrecht, The Netherlands.(Springer-Verlag LNCS 664.) (To appear in Mathematical Structures in Computer Science, 1995.)","DOI":"10.1007\/BFb0037117"},{"key":"S0956796800001775_ref009","doi-asserted-by":"crossref","unstructured":"Duba B. , Harper R. and MacQueen D. (1991) Typing first-class continuations in ML. 18th ACM Symposium on Principles of Programming Languages.","DOI":"10.1145\/99583.99608"},{"key":"S0956796800001775_ref029","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-15648-8_17"},{"key":"S0956796800001775_ref011","doi-asserted-by":"publisher","DOI":"10.1007\/BF01019461"},{"key":"S0956796800001775_ref038","first-page":"408","volume-title":"Colloq. sur la Programmation: Lecture Notes in Computer Science 19","author":"Reynolds","year":"1974"},{"key":"S0956796800001775_ref039","volume-title":"Preliminary design of the programming language Forsythe","author":"Reynolds","year":"1988"},{"key":"S0956796800001775_ref024","volume-title":"Report on the Programming Language Haskell, Version 1.0","author":"Hudak","year":"1990"},{"key":"S0956796800001775_ref040","doi-asserted-by":"publisher","DOI":"10.1007\/BF01019459"},{"key":"S0956796800001775_ref016","doi-asserted-by":"crossref","unstructured":"Griffin T. (1990) A formulae-as-types notion of control. 17th ACM Symposium on Principles of Programming Languages, San Francisco, CA.","DOI":"10.1145\/96709.96714"},{"key":"S0956796800001775_ref037","doi-asserted-by":"crossref","unstructured":"Reynolds J. C. (1972) Definitional interpreters for higher-order programming languages. Conference Record of the 25th National ACM Conference, pp. 717\u2013740, Boston, MA.","DOI":"10.1145\/800194.805852"},{"key":"S0956796800001775_ref023","doi-asserted-by":"publisher","DOI":"10.1016\/0096-0551(86)90007-X"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796800001775","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,12]],"date-time":"2019-05-12T17:40:38Z","timestamp":1557682838000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796800001775\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996,5]]},"references-count":42,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1996,5]]}},"alternative-id":["S0956796800001775"],"URL":"https:\/\/doi.org\/10.1017\/s0956796800001775","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996,5]]}}}