{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,10,26]],"date-time":"2023-10-26T10:22:21Z","timestamp":1698315741405},"reference-count":54,"publisher":"Cambridge University Press (CUP)","issue":"6","license":[{"start":{"date-parts":[[2007,11,1]],"date-time":"2007-11-01T00:00:00Z","timestamp":1193875200000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2007,11]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Asynchronous exceptions, or<jats:italic>interrupts<\/jats:italic>, are important for writing robust, modular programs, but are traditionally viewed as being difficult from a semantic perspective. In this article, we present a simple, formally justified, semantics for interrupts. Our approach is to show how a high-level semantics for interrupts can be justified with respect to a low-level implementation, by means of a compiler and its correctness theorem. In this manner we obtain two different perspectives on the problem, formally shown to be equivalent, which gives greater confidence in the correctness of our semantics.<\/jats:p>","DOI":"10.1017\/s0956796807006363","type":"journal-article","created":{"date-parts":[[2007,4,25]],"date-time":"2007-04-25T12:57:00Z","timestamp":1177505820000},"page":"777-792","source":"Crossref","is-referenced-by-count":13,"title":["What is the meaning of these constant interruptions?"],"prefix":"10.1017","volume":"17","author":[{"given":"GRAHAM","family":"HUTTON","sequence":"first","affiliation":[]},{"given":"JOEL","family":"WRIGHT","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2007,11,1]]},"reference":[{"key":"S0956796807006363_ref8","doi-asserted-by":"publisher","DOI":"10.1109\/32.877847"},{"key":"S0956796807006363_ref14","unstructured":"Drew S. , Gouph K. J. & Ledermann J. (1995) Implementing Zero Overhead Exception Handling. Tech. Rept. 95-12. Faculty of Information Technology, Queensland University of Technology."},{"key":"S0956796807006363_ref27","doi-asserted-by":"crossref","unstructured":"Jacobs B. (2001) A formalisation of Java's exception mechanism. In: ESOP 2001: Proceedings of the 10th European Symposium on Programming Languages and Systems. Springer-Verlag, pp. 284\u2013301.","DOI":"10.1007\/3-540-45309-1_19"},{"key":"S0956796807006363_ref19","unstructured":"Gordon A. (1995) Bisimilarity as a Theory of Functional Programming. BRICS Notes Series NS-95-3. Aarhus University."},{"key":"S0956796807006363_ref48","unstructured":"Sebesta R. W. (2006) Concepts of Programming Languages, 7th ed. Pearson Addison Wesley."},{"key":"S0956796807006363_ref3","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(89)90097-5"},{"key":"S0956796807006363_ref22","volume-title":"Communicating Sequential Processes","author":"Hoare","year":"1985"},{"key":"S0956796807006363_ref41","doi-asserted-by":"crossref","unstructured":"Palsberg J. & Ma D. (2002) A typed interrupt calculus. In: Proceedings of the 7th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems. Springer-Verlag, pp. 291\u2013310.","DOI":"10.1007\/3-540-45739-9_18"},{"key":"S0956796807006363_ref50","doi-asserted-by":"crossref","unstructured":"Thielecke H. (2000) On exceptions versus continuations in the presence of state. In: Proceedings of the 9th European Symposium on Programming Languages and Systems. Springer Verlag.","DOI":"10.1007\/3-540-46425-5_26"},{"key":"S0956796807006363_ref40","unstructured":"Nipkow T. (2004) Compiling exceptions correctly. Archive of Formal Proofs. Available at: http:\/\/afp.sourceforge.net\/."},{"key":"S0956796807006363_ref4","doi-asserted-by":"publisher","DOI":"10.1145\/504311.504284"},{"key":"S0956796807006363_ref1","doi-asserted-by":"crossref","unstructured":"Ager M. S. Biernacki D. Danvy O. & Midtgaard J. (2003) From Interpreter to Compiler and Virtual Machine: a Functional Derivation. Technical Report RS-03-14. BRICS, Aarhus, Denmark.","DOI":"10.7146\/brics.v10i14.21784"},{"key":"S0956796807006363_ref21","unstructured":"Hinze R. & L\u00f6h A. (2006) The lhs2TeX System for Typesetting Haskell. Available at: http:\/\/www.cs.uu.nl\/~andres\/lhs2tex\/."},{"key":"S0956796807006363_ref31","unstructured":"Leino K. , Rustan M. & Snepscheut van de , Jan L. A. (1994) Semantics of exceptions. In: Proceedings of the IFIP Working Conference on Programming Concepts, Methods and Calculi. North-Holland, pp. 447\u2013466."},{"key":"S0956796807006363_ref2","volume-title":"Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Aiken","year":"1990"},{"key":"S0956796807006363_ref30","doi-asserted-by":"crossref","unstructured":"Laird J. (2002) Exceptions, Continuations and Macro-expressiveness. In: Proceedings of the 11th European Symposium on Programming Languages and Systems. Springer Verlag.","DOI":"10.1007\/3-540-45927-8_10"},{"key":"S0956796807006363_ref16","unstructured":"Drossopoulou S. & Valkevych T. (2000) Java Exceptions Throw No Surprises. Technical report. Department of Computing, Imperial College of Science, Technology and Medicine."},{"key":"S0956796807006363_ref44","volume-title":"Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation","author":"Peyton","year":"1999"},{"key":"S0956796807006363_ref5","volume-title":"Compiling With Continuations","author":"Appel","year":"1992"},{"key":"S0956796807006363_ref36","unstructured":"Milner R. (1989) Communication and Concurrency. Prentice Hall."},{"key":"S0956796807006363_ref43","unstructured":"Peyton Jones, S. (2001) Tackling the awkward squad: Monadic input\/output, concurrency, exceptions, and foreign-language calls in Haskell. In: Engineering Theories of Software Construction Hoare T. Broy M. & Steinbruggen R. (eds), IOS Press. Presented at the 2000 Marktoberdorf Summer School."},{"key":"S0956796807006363_ref7","volume-title":"Program Construction: Calculating Implementations From Specifications","author":"Backhouse","year":"2003"},{"key":"S0956796807006363_ref9","first-page":"229","article-title":"Implemention of exception handling, Part I","volume":"5","author":"Chase","year":"1994","journal-title":"J. C Language Trans"},{"key":"S0956796807006363_ref29","doi-asserted-by":"crossref","unstructured":"Laird J. (2001) A fully abstract game semantics of local exceptions. In: Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society.","DOI":"10.1109\/LICS.2001.932487"},{"key":"S0956796807006363_ref17","doi-asserted-by":"publisher","DOI":"10.1016\/0096-0551(89)90018-0"},{"key":"S0956796807006363_ref23","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511813672"},{"key":"S0956796807006363_ref47","doi-asserted-by":"crossref","unstructured":"Riecke J. G. & Thielecke H. (1999) Typed exceptions and continuations cannot macro-express each other. In: Proceedings of the 26th International Colloquium on Automata, Languages and Programming. Springer Verlag.","DOI":"10.1007\/3-540-48523-6_60"},{"key":"S0956796807006363_ref10","first-page":"20","article-title":"Implemention of exception handling, Part II","volume":"6","author":"Chase","year":"1994","journal-title":"J. C Language Trans"},{"key":"S0956796807006363_ref12","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044482830-9\/50030-8"},{"key":"S0956796807006363_ref13","first-page":"68","volume-title":"Dependability of Resilient Computers","author":"Cristian","year":"1989"},{"key":"S0956796807006363_ref15","doi-asserted-by":"publisher","DOI":"10.1016\/0096-0551(94)90015-9"},{"key":"S0956796807006363_ref18","doi-asserted-by":"publisher","DOI":"10.1145\/361227.361230"},{"key":"S0956796807006363_ref20","doi-asserted-by":"publisher","DOI":"10.1145\/800055.802018"},{"key":"S0956796807006363_ref24","doi-asserted-by":"crossref","unstructured":"Hutton G. & Wright J. (2004) Compiling exceptions correctly. In: Proceedings of the 7th International Conference on Mathematics of Program Construction. Lecture Notes in Computer Science, vol. 3125. Stirling, Scotland: Springer.","DOI":"10.1007\/978-3-540-27764-4_12"},{"key":"S0956796807006363_ref25","doi-asserted-by":"crossref","unstructured":"Hutton G. & Wright J. (2006) Calculating an exceptional machine. Loidl, Hans-Wolfgang (ed), Trends in Functional Programming volume 5. Selected papers from the Fifth Symposium on Trends in Functional Programming, Munich, November 2004. Bristol: Intellect.","DOI":"10.2307\/j.ctv36xw0k5.7"},{"key":"S0956796807006363_ref26","doi-asserted-by":"crossref","unstructured":"Jacobs B. & Poll E. (2003) Java Program Verification at Nijmegen: Developments and Perspective. Technical Report NIII-R0318. Nijmegen Institute for Computing and Information Sciences.","DOI":"10.1007\/978-3-540-37621-7_7"},{"key":"S0956796807006363_ref34","unstructured":"McBride C. , McKinna J. & Altenkirch T. (2006) The epigram system. Available at: http:\/\/www.e-pig.org\/."},{"key":"S0956796807006363_ref28","doi-asserted-by":"publisher","DOI":"10.1145\/1146809.1146811"},{"key":"S0956796807006363_ref32","doi-asserted-by":"publisher","DOI":"10.1023\/A:1010020917337"},{"key":"S0956796807006363_ref33","volume-title":"Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation","author":"Marlow","year":"2001"},{"key":"S0956796807006363_ref35","unstructured":"McKinna J. & Wright J. (2006, July) Towards type-correct, provably correct, compilers: A case study in epigram. J. Funct. Program."},{"key":"S0956796807006363_ref42","doi-asserted-by":"crossref","first-page":"340","DOI":"10.1145\/349214.349230","article-title":"Type-based analysis of uncaught exceptions","volume":"22","author":"Pessaux","year":"2000","journal-title":"ACM Trans. Program. Languages Syst"},{"key":"S0956796807006363_ref37","volume-title":"Communicating and Mobile Systems: The \u03c0-Calculus","author":"Milner","year":"1999"},{"key":"S0956796807006363_ref38","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2319.001.0001","volume-title":"The Definition of Standard ML (Revised)","author":"Milner","year":"1997"},{"key":"S0956796807006363_ref39","article-title":"Imprecise exceptions, co-inductively","volume":"26","author":"Moran","year":"1999","journal-title":"Electron. Notes Theor. Comp. Sci"},{"key":"S0956796807006363_ref51","volume-title":"Constructivism in Mathematics: An Introduction","author":"Troelstra","year":"1988"},{"key":"S0956796807006363_ref49","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(90)90056-J"},{"key":"S0956796807006363_ref52","volume-title":"Proceedings of the 7th International Conference on Functional Programming and Computer Architecture","author":"Wand","year":"1995"},{"key":"S0956796807006363_ref53","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"},{"key":"S0956796807006363_ref46","first-page":"717","volume-title":"Proceedings of the ACM Annual Conference","author":"Reynolds","year":"1972"},{"key":"S0956796807006363_ref11","volume-title":"Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming","author":"Claessen","year":"2000"},{"key":"S0956796807006363_ref54","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00317-0"},{"key":"S0956796807006363_ref45","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349337"},{"key":"S0956796807006363_ref6","volume-title":"American National Standard \u2013 Programming Language PL\/I","author":"Auwaerter","year":"1976"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796807006363","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,11]],"date-time":"2023-05-11T15:39:03Z","timestamp":1683819543000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796807006363\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,11]]},"references-count":54,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2007,11]]}},"alternative-id":["S0956796807006363"],"URL":"https:\/\/doi.org\/10.1017\/s0956796807006363","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,11]]}}}