{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:52:54Z","timestamp":1740099174809,"version":"3.37.3"},"publisher-location":"Cham","reference-count":17,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030027674"},{"type":"electronic","value":"9783030027681"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"tdm","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":[[2018]]},"DOI":"10.1007\/978-3-030-02768-1_7","type":"book-chapter","created":{"date-parts":[[2018,10,21]],"date-time":"2018-10-21T07:42:27Z","timestamp":1540107747000},"page":"131-145","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Scallina: Translating Verified Programs from Coq to Scala"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4414-3161","authenticated-orcid":false,"given":"Youssef","family":"El Bakouny","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dani","family":"Mezher","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,10,22]]},"reference":[{"key":"7_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-3-319-30936-1_14","volume-title":"A List of Successes That Can Change the World","author":"N Amin","year":"2016","unstructured":"Amin, N., Gr\u00fctter, S., Odersky, M., Rompf, T., Stucki, S.: The Essence of dependent object types. In: Lindley, S., McBride, C., Trinder, P., Sannella, D. (eds.) A List of Successes That Can Change the World. LNCS, vol. 9600, pp. 249\u2013272. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-30936-1_14"},{"key":"7_CR2","unstructured":"Appel, A.W.: Verified Functional Algorithms, Software Foundations, vol. 3 (2017). Edited by Pierce, B.C."},{"issue":"1","key":"7_CR3","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/s10516-014-9260-9","volume":"25","author":"N Guallart","year":"2015","unstructured":"Guallart, N.: An overview of type theories. Axiomathes 25(1), 61\u201377 (2015). \nhttps:\/\/doi.org\/10.1007\/s10516-014-9260-9","journal-title":"Axiomathes"},{"key":"7_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/978-3-642-12251-4_9","volume-title":"Functional and Logic Programming","author":"F Haftmann","year":"2010","unstructured":"Haftmann, F., Nipkow, T.: Code generation via higher-order rewrite systems. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) FLOPS 2010. LNCS, vol. 6009, pp. 103\u2013117. Springer, Heidelberg (2010). \nhttps:\/\/doi.org\/10.1007\/978-3-642-12251-4_9"},{"key":"7_CR5","first-page":"29","volume":"146","author":"R Hindley","year":"1969","unstructured":"Hindley, R.: The principle type-scheme of an object in combinatory logic. Trans. Am. Math. Soc. 146, 29\u201360 (1969)","journal-title":"Trans. Am. Math. Soc."},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"568","DOI":"10.1007\/978-3-319-40229-1_38","volume-title":"Automated Reasoning","author":"L Hupel","year":"2016","unstructured":"Hupel, L., Kuncak, V.: Translating scala programs to isabelle\/HOL. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 568\u2013577. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-40229-1_38"},{"key":"7_CR7","doi-asserted-by":"publisher","unstructured":"Klein, G., et al.: seL4: formal verification of an OS kernel. In: Matthews, J.N., Anderson, T.E. (eds.) Proceedings of the 22nd ACM Symposium on Operating Systems Principles 2009, SOSP 2009, Big Sky, Montana, USA, 11\u201314 October 2009, pp. 207\u2013220. ACM (2009). \nhttps:\/\/doi.org\/10.1145\/1629575.1629596","DOI":"10.1145\/1629575.1629596"},{"key":"7_CR8","doi-asserted-by":"publisher","unstructured":"Leroy, X.: Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In: Morrisett, J.G., Jones, S.L.P. (eds.) Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006, Charleston, South Carolina, USA, 11\u201313 January 2006, pp. 42\u201354. ACM (2006). \nhttps:\/\/doi.org\/10.1145\/1111037.1111042","DOI":"10.1145\/1111037.1111042"},{"key":"7_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/3-540-39185-1_12","volume-title":"Types for Proofs and Programs","author":"P Letouzey","year":"2003","unstructured":"Letouzey, P.: A new extraction for Coq. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol. 2646, pp. 200\u2013219. Springer, Heidelberg (2003). \nhttps:\/\/doi.org\/10.1007\/3-540-39185-1_12"},{"key":"7_CR10","unstructured":"Letouzey, P.: Programmation fonctionnelle certifi\u00e9e : L\u2019extraction de programmes dans l\u2019assistant Coq. (Certified functional programming: Program extraction within Coq proof assistant), Ph.D. thesis, University of Paris-Sud, Orsay, France (2004). \nhttps:\/\/tel.archives-ouvertes.fr\/tel-00150912"},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/978-3-540-69407-6_39","volume-title":"Logic and Theory of Algorithms","author":"P Letouzey","year":"2008","unstructured":"Letouzey, P.: Extraction in Coq: an overview. In: Beckmann, A., Dimitracopoulos, C., L\u00f6we, B. (eds.) CiE 2008. LNCS, vol. 5028, pp. 359\u2013369. Springer, Heidelberg (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-69407-6_39"},{"key":"7_CR12","unstructured":"The Coq development team: The Coq proof assistant reference manual, version 8.0. LogiCal Project (2004). \nhttp:\/\/coq.inria.fr"},{"issue":"3","key":"7_CR13","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1016\/0022-0000(78)90014-4","volume":"17","author":"R Milner","year":"1978","unstructured":"Milner, R.: A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17(3), 348\u2013375 (1978). \nhttps:\/\/doi.org\/10.1016\/0022-0000(78)90014-4","journal-title":"J. Comput. Syst. Sci."},{"key":"7_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL - A Proof Assistant for Higher-order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL - A Proof Assistant for Higher-order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). \nhttps:\/\/doi.org\/10.1007\/3-540-45949-9"},{"issue":"4","key":"7_CR15","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1145\/2591013","volume":"57","author":"M Odersky","year":"2014","unstructured":"Odersky, M., Rompf, T.: Unifying functional and object-oriented programming with scala. Commun. ACM 57(4), 76\u201386 (2014). \nhttps:\/\/doi.org\/10.1145\/2591013","journal-title":"Commun. ACM"},{"key":"7_CR16","volume-title":"Programming in Scala: A Comprehensive Step-by-step Guide","author":"M Odersky","year":"2011","unstructured":"Odersky, M., Spoon, L., Venners, B.: Programming in Scala: A Comprehensive Step-by-step Guide, 2nd edn. Artima Incorporation, Walnut Creek (2011)","edition":"2"},{"key":"7_CR17","doi-asserted-by":"publisher","unstructured":"Pierce, B.C.: The science of deep specification (keynote). In: Visser, E. (ed.) Companion Proceedings of the 2016 ACM SIGPLAN International Conference on Systems, Programming, Languages and Applications: Software for Humanity, SPLASH 2016, Amsterdam, Netherlands, 30 October\u20134 November 2016, p. 1. ACM (2016). \nhttps:\/\/doi.org\/10.1145\/2984043.2998388","DOI":"10.1145\/2984043.2998388"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-02768-1_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,10,21]],"date-time":"2018-10-21T07:44:39Z","timestamp":1540107879000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-02768-1_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783030027674","9783030027681"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-02768-1_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"APLAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Asian Symposium on Programming Languages and Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Wellington","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"New Zealand","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 December 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 December 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"aplas2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/aplas2018.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}