{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:20:30Z","timestamp":1750220430047,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":33,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,9,25]],"date-time":"2019-09-25T00:00:00Z","timestamp":1569369600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100007601","name":"Horizon 2020","doi-asserted-by":"publisher","award":["779882"],"award-info":[{"award-number":["779882"]}],"id":[{"id":"10.13039\/501100007601","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/P020631\/1"],"award-info":[{"award-number":["EP\/P020631\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2019,9,25]]},"DOI":"10.1145\/3412932.3412944","type":"proceedings-article","created":{"date-parts":[[2021,7,15]],"date-time":"2021-07-15T16:08:45Z","timestamp":1626365325000},"page":"1-12","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["A trustworthy framework for resource-aware embedded programming"],"prefix":"10.1145","author":[{"given":"Adam D.","family":"Barwell","sequence":"first","affiliation":[{"name":"University of St Andrews, Scotland, UK"}]},{"given":"Christopher","family":"Brown","sequence":"additional","affiliation":[{"name":"University of St Andrews, Scotland, UK"}]}],"member":"320","published-online":{"date-parts":[[2021,7,15]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"2011. XC Specification ver. 1.0 (X5965A). https:\/\/www.xmos.com\/developer\/xc-specification.  2011. XC Specification ver. 1.0 (X5965A). https:\/\/www.xmos.com\/developer\/xc-specification."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068410000487"},{"volume-title":"LOPSTR (Lecture Notes in Computer Science)","author":"Bacci Giovanni","key":"e_1_3_2_1_3_1","unstructured":"Giovanni Bacci and Marco Comini . 2010. Abstract Diagnosis of First Order Functional Logic Programs . In LOPSTR (Lecture Notes in Computer Science) , Vol. 6564 . Springer , 215--233. Giovanni Bacci and Marco Comini. 2010. Abstract Diagnosis of First Order Functional Logic Programs. In LOPSTR (Lecture Notes in Computer Science), Vol. 6564. Springer, 215--233."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"crossref","unstructured":"Fran\u00e7ois Bourdoncle. 1993. Abstract Debugging of Higher-Order Imperative Languages. In PLDI. ACM 46--55.  Fran\u00e7ois Bourdoncle. 1993. Abstract Debugging of Higher-Order Imperative Languages. In PLDI. ACM 46--55.","DOI":"10.1145\/173262.155095"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681300018X"},{"key":"e_1_3_2_1_6_1","unstructured":"Christopher Brown Adam D. Barwell Yoann Marquer C\u00e9line Minh and Olivier Zendra. 2019. Type-Driven Verification of Non-functional Properties. In PPDP. Accepted for publication.  Christopher Brown Adam D. Barwell Yoann Marquer C\u00e9line Minh and Olivier Zendra. 2019. Type-Driven Verification of Non-functional Properties. In PPDP. Accepted for publication."},{"volume-title":"A Permission-Dependent Type System for Secure Information Flow Analysis","author":"Chen Hongxu","key":"e_1_3_2_1_7_1","unstructured":"Hongxu Chen , Alwen Tiu , Zhiwu Xu , and Yang Liu . 2018. A Permission-Dependent Type System for Secure Information Flow Analysis . In CSF. IEEE Computer Society , 218--232. Hongxu Chen, Alwen Tiu, Zhiwu Xu, and Yang Liu. 2018. A Permission-Dependent Type System for Secure Information Flow Analysis. In CSF. IEEE Computer Society, 218--232."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1012996816178"},{"key":"e_1_3_2_1_9_1","volume-title":"Acar","author":"\u00c7i\u00e7ek Ezgi","year":"2015","unstructured":"Ezgi \u00c7i\u00e7ek , Deepak Garg , and Umut A . Acar . 2015 . Refinement Types for Incremental Computational Complexity. In ESOP (Lecture Notes in Computer Science), Vol. 9032 . Springer , 406--431. Ezgi \u00c7i\u00e7ek, Deepak Garg, and Umut A. Acar. 2015. Refinement Types for Incremental Computational Complexity. In ESOP (Lecture Notes in Computer Science), Vol. 9032. Springer, 406--431."},{"volume-title":"VMCAI (Lecture Notes in Computer Science)","author":"Cousot Patrick","key":"e_1_3_2_1_10_1","unstructured":"Patrick Cousot . 2003. Automatic Verification by Abstract Interpretation . In VMCAI (Lecture Notes in Computer Science) , Vol. 2575 . Springer , 20--24. Patrick Cousot. 2003. Automatic Verification by Abstract Interpretation. In VMCAI (Lecture Notes in Computer Science), Vol. 2575. Springer, 20--24."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11241-010-9101-x"},{"key":"e_1_3_2_1_13_1","volume-title":"Energy Transparency for Deeply Embedded Programs. TACO 14, 1","author":"Georgiou Kyriakos","year":"2017","unstructured":"Kyriakos Georgiou , Steve Kerrison , Zbigniew Chamski , and Kerstin Eder . 2017. Energy Transparency for Deeply Embedded Programs. TACO 14, 1 ( 2017 ), 8:1--8:26. Kyriakos Georgiou, Steve Kerrison, Zbigniew Chamski, and Kerstin Eder. 2017. Energy Transparency for Deeply Embedded Programs. TACO 14, 1 (2017), 8:1--8:26."},{"key":"e_1_3_2_1_14_1","volume-title":"Java SE 8 Edition","author":"Gosling James","unstructured":"James Gosling , Bill Joy , Guy L. Steele , Gilad Bracha , and Alex Buckley . 2014. The Java Language Specification , Java SE 8 Edition ( 1 st ed.). Addison-Wesley Professional . James Gosling, Bill Joy, Guy L. Steele, Gilad Bracha, and Alex Buckley. 2014. The Java Language Specification, Java SE 8 Edition (1st ed.). Addison-Wesley Professional.","edition":"1"},{"key":"e_1_3_2_1_15_1","volume-title":"Chilimbi","author":"Gulwani Sumit","year":"2009","unstructured":"Sumit Gulwani , Krishna K. Mehra , and Trishul M . Chilimbi . 2009 . SPEED: precise and efficient static estimation of program computational complexity. In POPL. ACM , 127--139. Sumit Gulwani, Krishna K. Mehra, and Trishul M. Chilimbi. 2009. SPEED: precise and efficient static estimation of program computational complexity. In POPL. ACM, 127--139."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2005.02.006"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2362389.2362393"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"crossref","unstructured":"John Hughes and Lars Pareto. 1999. Recursion and Dynamic Data-structures in Bounded Space: Towards Embedded ML Programming. In ICFP. ACM 70--81.  John Hughes and Lars Pareto. 1999. Recursion and Dynamic Data-structures in Bounded Space: Towards Embedded ML Programming. In ICFP. ACM 70--81.","DOI":"10.1145\/317765.317785"},{"volume-title":"Programming in Haskell","author":"Hutton Graham","key":"e_1_3_2_1_19_1","unstructured":"Graham Hutton . 2007. Programming in Haskell . Cambridge University Press , New York, NY, USA . Graham Hutton. 2007. Programming in Haskell. Cambridge University Press, New York, NY, USA."},{"volume-title":"RSA, DSS, and Other Systems. In CRYPTO (Lecture Notes in Computer Science)","author":"Kocher Paul C.","key":"e_1_3_2_1_20_1","unstructured":"Paul C. Kocher . 1996. Timing Attacks on Implementations of Diffie-Hellman , RSA, DSS, and Other Systems. In CRYPTO (Lecture Notes in Computer Science) , Vol. 1109 . Springer , 104--113. Paul C. Kocher. 1996. Timing Attacks on Implementations of Diffie-Hellman, RSA, DSS, and Other Systems. In CRYPTO (Lecture Notes in Computer Science), Vol. 1109. Springer, 104--113."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"crossref","unstructured":"Ugo Dal Lago and Barbara Petit. 2013. The geometry of types. In POPL. ACM 167--178.  Ugo Dal Lago and Barbara Petit. 2013. The geometry of types. In POPL. ACM 167--178.","DOI":"10.1145\/2480359.2429090"},{"volume-title":"LOPSTR (Lecture Notes in Computer Science)","author":"Liqat Umer","key":"e_1_3_2_1_22_1","unstructured":"Umer Liqat , Steve Kerrison , Alejandro Serrano , Kyriakos Georgiou , Pedro L\u00f3pez-Garc\u00eda , Neville Grech , Manuel V. Hermenegildo , and Kerstin Eder . 2013. Energy Consumption Analysis of Programs Based on XMOS ISA-Level Models . In LOPSTR (Lecture Notes in Computer Science) , Vol. 8901 . Springer , 72--90. Umer Liqat, Steve Kerrison, Alejandro Serrano, Kyriakos Georgiou, Pedro L\u00f3pez-Garc\u00eda, Neville Grech, Manuel V. Hermenegildo, and Kerstin Eder. 2013. Energy Consumption Analysis of Programs Based on XMOS ISA-Level Models. In LOPSTR (Lecture Notes in Computer Science), Vol. 8901. Springer, 72--90."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068418000042"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3173042"},{"volume-title":"Proof-Carrying Code","author":"Necula George C.","key":"e_1_3_2_1_25_1","unstructured":"George C. Necula . 1997. Proof-Carrying Code . In POPL. ACM Press , 106--119. George C. Necula. 1997. Proof-Carrying Code. In POPL. ACM Press, 106--119."},{"volume-title":"Semantics with Applications: An Appetizer","author":"Nielson Hanne Riis","key":"e_1_3_2_1_26_1","unstructured":"Hanne Riis Nielson and Flemming Nielson . 2007. Semantics with Applications: An Appetizer . Springer . Hanne Riis Nielson and Flemming Nielson. 2007. Semantics with Applications: An Appetizer. Springer."},{"key":"e_1_3_2_1_27_1","volume-title":"BEEBS: Open Benchmarks for Energy Measurements on Embedded Platforms. CoRR abs\/1308.5174","author":"Pallister James","year":"2013","unstructured":"James Pallister , Simon J. Hollis , and Jeremy Bennett . 2013 . BEEBS: Open Benchmarks for Energy Measurements on Embedded Platforms. CoRR abs\/1308.5174 (2013). arXiv:1308.5174 http:\/\/arxiv.org\/abs\/1308.5174 James Pallister, Simon J. Hollis, and Jeremy Bennett. 2013. BEEBS: Open Benchmarks for Energy Measurements on Embedded Platforms. CoRR abs\/1308.5174 (2013). arXiv:1308.5174 http:\/\/arxiv.org\/abs\/1308.5174"},{"volume-title":"PADL (Lecture Notes in Computer Science)","author":"Schwaab Christopher","key":"e_1_3_2_1_28_1","unstructured":"Christopher Schwaab , Ekaterina Komendantskaya , Alasdair Hill , Frantisek Farka , Ronald P. A. Petrick , Joe B. Wells , and Kevin Hammond . 2019. Proof-Carrying Plans . In PADL (Lecture Notes in Computer Science) , Vol. 11372 . Springer , 204--220. Christopher Schwaab, Ekaterina Komendantskaya, Alasdair Hill, Frantisek Farka, Ronald P. A. Petrick, Joe B. Wells, and Kevin Hammond. 2019. Proof-Carrying Plans. In PADL (Lecture Notes in Computer Science), Vol. 11372. Springer, 204--220."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1017\/S147106841400057X"},{"volume-title":"CICM (Lecture Notes in Computer Science)","author":"Slama Franck","key":"e_1_3_2_1_30_1","unstructured":"Franck Slama and Edwin Brady . 2017. Automatically Proving Equivalence by Type-Safe Reflection . In CICM (Lecture Notes in Computer Science) , Vol. 10383 . Springer , 40--55. Franck Slama and Edwin Brady. 2017. Automatically Proving Equivalence by Type-Safe Reflection. In CICM (Lecture Notes in Computer Science), Vol. 10383. Springer, 40--55."},{"volume-title":"Homotopy Type Theory: Univalent Foundations of Mathematics. https:\/\/homotopytypetheory.org\/book","author":"Foundations Program The Univalent","key":"e_1_3_2_1_31_1","unstructured":"The Univalent Foundations Program . 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. https:\/\/homotopytypetheory.org\/book , Institute for Advanced Study . The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. https:\/\/homotopytypetheory.org\/book, Institute for Advanced Study."},{"key":"e_1_3_2_1_32_1","volume-title":"Vasconcelos and Kevin Hammond","author":"Pedro","year":"2003","unstructured":"Pedro B. Vasconcelos and Kevin Hammond . 2003 . Inferring Cost Equations for Recursive, Polymorphic and Higher-Order Functional Programs. In IFL (Lecture Notes in Computer Science), Vol. 3145 . Springer , 86--101. Pedro B. Vasconcelos and Kevin Hammond. 2003. Inferring Cost Equations for Recursive, Polymorphic and Higher-Order Functional Programs. In IFL (Lecture Notes in Computer Science), Vol. 3145. Springer, 86--101."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/353629.353648"}],"event":{"name":"IFL '19: Implementation and Application of Functional Languages","acronym":"IFL '19","location":"Singapore Singapore"},"container-title":["Proceedings of the 31st Symposium on Implementation and Application of Functional Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3412932.3412944","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3412932.3412944","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:47:02Z","timestamp":1750193222000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3412932.3412944"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,9,25]]},"references-count":33,"alternative-id":["10.1145\/3412932.3412944","10.1145\/3412932"],"URL":"https:\/\/doi.org\/10.1145\/3412932.3412944","relation":{},"subject":[],"published":{"date-parts":[[2019,9,25]]},"assertion":[{"value":"2021-07-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}