{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,12]],"date-time":"2026-04-12T17:05:44Z","timestamp":1776013544300,"version":"3.50.1"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319893655","type":"print"},{"value":"9783319893662","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-89366-2_8","type":"book-chapter","created":{"date-parts":[[2018,4,13]],"date-time":"2018-04-13T19:52:34Z","timestamp":1523649154000},"page":"146-162","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Fab ous Interoperability for ML and a Linear Language"],"prefix":"10.1007","author":[{"given":"Gabriel","family":"Scherer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Max","family":"New","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nick","family":"Rioux","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Amal","family":"Ahmed","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,4,14]]},"reference":[{"issue":"2","key":"8_CR1","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1006\/inco.2000.2930","volume":"163","author":"S Abramsky","year":"2000","unstructured":"Abramsky, S., Jagadeesan, R., Malacaria, P.: Full abstraction for PCF. Inf. Comput. 163(2), 409\u2013470 (2000)","journal-title":"Inf. Comput."},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Ahmed, A., Blume, M.: Typed closure conversion preserves observational equivalence. In: International Conference on Functional Programming (ICFP), Victoria, British Columbia, Canada, pp. 157\u2013168, September 2008","DOI":"10.1145\/1411204.1411227"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"Ahmed, A., Blume, M.: An equivalence-preserving CPS translation via multi-language semantics. In: International Conference on Functional Programming (ICFP), Tokyo, Japan, pp. 431\u2013444, September 2011","DOI":"10.1145\/2034773.2034830"},{"issue":"4","key":"8_CR4","first-page":"397","volume":"77","author":"A Ahmed","year":"2007","unstructured":"Ahmed, A., Fluet, M., Morrisett, G.: L3: a linear language with locations. Fundamenta Informaticae 77(4), 397\u2013449 (2007)","journal-title":"Fundamenta Informaticae"},{"issue":"4","key":"8_CR5","doi-asserted-by":"publisher","first-page":"14:1","DOI":"10.1145\/2837022","volume":"38","author":"T Balabonski","year":"2016","unstructured":"Balabonski, T., Pottier, F., Protzenko, J.: The design and formalization of Mezzo, a permission-based programming language. ACM Trans. Program. Lang. Syst. 38(4), 14:1\u201314:94 (2016)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"8_CR6","unstructured":"Barrett, E., Bolz, C.F., Diekmann, L., Tratt, L.: Fine-grained language composition: a case study. In: ECOOP (2016)"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/BFb0022251","volume-title":"Computer Science Logic","author":"PN Benton","year":"1995","unstructured":"Benton, P.N.: A mixed linear and non-linear logic: proofs, terms and models. In: Pacholski, L., Tiuryn, J. (eds.) CSL 1994. LNCS, vol. 933, pp. 121\u2013135. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/BFb0022251"},{"issue":"POPL","key":"8_CR8","doi-asserted-by":"publisher","first-page":"5:1","DOI":"10.1145\/3158093","volume":"2","author":"J-P Bernardy","year":"2018","unstructured":"Bernardy, J.-P., Boespflug, M., Newton, R.R., Jones, S.P., Spiwack, A.: Linear haskell: practical linearity in a higher-order polymorphic language. PACMPL 2(POPL), 5:1\u20135:29 (2018). https:\/\/doi.org\/10.1145\/3158093","journal-title":"PACMPL"},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Cartwright, R., Felleisen, M.: Observable sequentiality and full abstraction. In: ACM Symposium on Principles of Programming Languages (POPL), Albuquerque, New Mexico, pp. 328\u2013342 (1992)","DOI":"10.1145\/143165.143232"},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"Devriese, D., Patrignani, M., Piessens, F.: Fully-abstract compilation by approximate back-translation. In: ACM Symposium on Principles of Programming Languages (POPL), St. Petersburg, Florida (2016)","DOI":"10.1145\/2837614.2837618"},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"Fahndrich, M., DeLine, R.: Adoption and focus: practical linear types for imperative programming. In: PLDI 2002 (2002)","DOI":"10.1145\/512529.512532"},{"issue":"1","key":"8_CR12","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1076\/csed.14.1.55.23499","volume":"14","author":"M Felleisen","year":"2004","unstructured":"Felleisen, M., Findler, R.B., Flatt, M., Krishnamurthi, S.: The teachscheme! project: computing and programming for every student. Comput. Sci. Educ. 14(1), 55\u201377 (2004)","journal-title":"Comput. Sci. Educ."},{"key":"8_CR13","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1145\/2629609","volume":"36","author":"R Garcia","year":"2014","unstructured":"Garcia, R., Tanter, \u00c9., Wolff, R., Aldrich, J.: Foundations of typestate-oriented programming. TOPLAS 36, 12 (2014)","journal-title":"TOPLAS"},{"key":"8_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"781","DOI":"10.1007\/978-3-642-31424-7_64","volume-title":"Computer Aided Verification","author":"J Hoffmann","year":"2012","unstructured":"Hoffmann, J., Aehlig, K., Hofmann, M.: Resource aware ML. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 781\u2013786. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_64"},{"key":"8_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/978-3-540-31987-0_29","volume-title":"Programming Languages and Systems","author":"A Jeffrey","year":"2005","unstructured":"Jeffrey, A., Rathke, J.: Java JR: fully\u00a0abstract\u00a0trace\u00a0semantics for\u00a0a\u00a0Core\u00a0Java\u00a0Language. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 423\u2013438. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31987-0_29"},{"issue":"3","key":"8_CR16","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1145\/1498926.1498930","volume":"31","author":"J Matthews","year":"2009","unstructured":"Matthews, J., Findler, R.B.: Operational semantics for multi-language programs. ACM Trans. Program. Lang. Syst. (TOPLAS) 31(3), 12 (2009)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"Meyer, A.R., Sieber, K.: Towards fully abstract semantics for local variables. In: ACM Symposium on Principles of Programming Languages (POPL), San Diego, California, pp. 191\u2013203 (1988)","DOI":"10.1145\/73560.73577"},{"issue":"1","key":"8_CR18","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(77)90053-6","volume":"4","author":"R Milner","year":"1977","unstructured":"Milner, R.: Fully abstract models of typed lambda calculi. Theor. Comput. Sci. 4(1), 1\u201322 (1977)","journal-title":"Theor. Comput. Sci."},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"Morris, J.G.: The best of both worlds: linear functional programming without compromise. In: ICFP (2016)","DOI":"10.1145\/2951913.2951925"},{"key":"8_CR20","doi-asserted-by":"crossref","unstructured":"New, M.S., Bowman, W.J., Ahmed, A.: Fully abstract compilation via universal embedding. In: International Conference on Functional Programming (ICFP), Nara, Japan, September 2016","DOI":"10.1145\/2951913.2951941"},{"key":"8_CR21","doi-asserted-by":"crossref","unstructured":"O\u2019Connor, L., Chen, Z., Rizkallah, C., Amani, S., Lim, J., Murray, T., Nagashima, Y., Sewell, T., Klein, G.: Refinement through restraint: bringing down the cost of verification. In: ICFP (2016)","DOI":"10.1145\/2951913.2951940"},{"key":"8_CR22","doi-asserted-by":"crossref","unstructured":"Osera, P.M., Sj\u00f6berg, V., Zdancewic, S.: Dependent interoperability. In: Programming Languages Meets Program Verification (PLPV), January 2012","DOI":"10.1145\/2103776.2103779"},{"issue":"2","key":"8_CR23","doi-asserted-by":"publisher","first-page":"6:1","DOI":"10.1145\/2699503","volume":"37","author":"M Patrignani","year":"2015","unstructured":"Patrignani, M., Agten, P., Strackx, R., Jacobs, B., Clarke, D., Piessens, F.: Secure compilation to protected module architectures. ACM Trans. Program. Lang. Syst. 37(2), 6:1\u20136:50 (2015)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"8_CR24","doi-asserted-by":"crossref","unstructured":"Patterson, D., Perconti, J., Dimoulas, C., Ahmed, A.: FunTAL: reasonably mixing a functional language with assembly. In: ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Barcelona, Spain, June 2017. http:\/\/www.ccs.neu.edu\/home\/amal\/papers\/funtal.pdf","DOI":"10.1145\/3062341.3062347"},{"key":"8_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/978-3-642-54833-8_8","volume-title":"Programming Languages and Systems","author":"JT Perconti","year":"2014","unstructured":"Perconti, J.T., Ahmed, A.: Verifying an open compiler using multi-language semantics. In: Shao, Z. (ed.) ESOP 2014. LNCS, vol. 8410, pp. 128\u2013148. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54833-8_8"},{"key":"8_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"550","DOI":"10.1007\/978-3-642-11957-6_29","volume-title":"Programming Languages and Systems","author":"JA Tov","year":"2010","unstructured":"Tov, J.A., Pucella, R.: Stateful contracts for affine types. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 550\u2013569. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-11957-6_29"},{"key":"8_CR27","doi-asserted-by":"crossref","unstructured":"Tov, J.A., Pucella, R.: Practical affine types. In: POPL (2011)","DOI":"10.1145\/1926385.1926436"},{"key":"8_CR28","unstructured":"Wadler, P.: Linear types can change the world! In: Programming Concepts and Methods (1990)"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-89366-2_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,15]],"date-time":"2019-10-15T16:20:54Z","timestamp":1571156454000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-89366-2_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319893655","9783319893662"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-89366-2_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}