{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:28:28Z","timestamp":1750220908044,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":51,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,10,7]],"date-time":"2019-10-07T00:00:00Z","timestamp":1570406400000},"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 Framework Programme","doi-asserted-by":"publisher","award":["779882"],"award-info":[{"award-number":["779882"]}],"id":[{"id":"10.13039\/501100007601","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2019,10,7]]},"DOI":"10.1145\/3354166.3354171","type":"proceedings-article","created":{"date-parts":[[2019,9,24]],"date-time":"2019-09-24T12:58:36Z","timestamp":1569329916000},"page":"1-15","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Type-Driven Verification of Non-functional Properties"],"prefix":"10.1145","author":[{"given":"Christopher","family":"Brown","sequence":"first","affiliation":[{"name":"University of St Andrews, Scotland, UK"}]},{"given":"Adam D.","family":"Barwell","sequence":"additional","affiliation":[{"name":"University of St Andrews, Scotland, UK"}]},{"given":"Yoann","family":"Marquer","sequence":"additional","affiliation":[{"name":"Inria, Univ Rennes, CNRS, IRISA, France"}]},{"given":"C\u00e9line","family":"Minh","sequence":"additional","affiliation":[{"name":"Inria, Univ Rennes, CNRS, IRISA, France"}]},{"given":"Olivier","family":"Zendra","sequence":"additional","affiliation":[{"name":"Inria, Univ Rennes, CNRS, IRISA, France"}]}],"member":"320","published-online":{"date-parts":[[2019,10,7]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"https:\/\/www.xmos.com\/developer\/xc-specification","author":"Xc","year":"2011","unstructured":"Xc specification ver. 1.0 (x5965a) ( 2011 ), https:\/\/www.xmos.com\/developer\/xc-specification Xc specification ver. 1.0 (x5965a) (2011), https:\/\/www.xmos.com\/developer\/xc-specification"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068410000487"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/TVLSI.2009.2030199"},{"key":"e_1_3_2_1_4_1","first-page":"1","volume-title":"La Padula","author":"Bell D.E.","year":"1976","unstructured":"Bell , D.E. , La Padula , L.J. : Secure computer system: Unified exposition and multics interpretation. In : Tech report ESD-TR-75-306. pp. 1 -- 133 . Mitre Corp, Bedford, Ma . ( 1976 ) Bell, D.E., La Padula, L.J.: Secure computer system: Unified exposition and multics interpretation. In: Tech report ESD-TR-75-306. pp. 1--133. Mitre Corp, Bedford, Ma. (1976)"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1929529.1929536"},{"key":"e_1_3_2_1_6_1","first-page":"218","volume-title":"Liu, Y.: A permission-dependent type system for secure information flow analysis","author":"Chen H.","year":"2018","unstructured":"Chen , H. , Tiu , A. , Xu , Z. , Liu, Y.: A permission-dependent type system for secure information flow analysis . In : CSF. pp. 218 -- 232 . IEEE Computer Society ( 2018 ) Chen, H., Tiu, A., Xu, Z., Liu, Y.: A permission-dependent type system for secure information flow analysis. In: CSF. pp. 218--232. IEEE Computer Society (2018)"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1012996816178"},{"key":"e_1_3_2_1_8_1","first-page":"406","volume-title":"ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings.","author":"\u00c7i\u00e7ek E.","year":"2015","unstructured":"\u00c7i\u00e7ek , E. , Garg , D. , Acar , U.A. : Refinement types for incremental computational complexity. In: Programming Languages and Systems - 24th European Symposium on Programming , ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings. pp. 406 -- 431 ( 2015 ). https:\/\/doi.org\/10.1007\/978-3-662-46669-8_17, https:\/\/doi.org\/10.1007\/978-3-662-46669-8_17 10.1007\/978-3-662-46669-8_17 \u00c7i\u00e7ek, E., Garg, D., Acar, U.A.: Refinement types for incremental computational complexity. In: Programming Languages and Systems - 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings. pp. 406--431 (2015). https:\/\/doi.org\/10.1007\/978-3-662-46669-8_17, https:\/\/doi.org\/10.1007\/978-3-662-46669-8_17"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.1987.10001"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1840845.1840883"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/CCST.2017.8167844"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11241-010-9101-x"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11241-010-9101-x"},{"key":"e_1_3_2_1_15_1","first-page":"794","volume-title":"F.: A uniform approach for the definition of security properties","author":"Focardi R.","year":"1999","unstructured":"Focardi , R. , Martinelli , F.: A uniform approach for the definition of security properties . In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM'99 -- Formal Methods. pp. 794 -- 813 . Springer Berlin Heidelberg , Berlin, Heidelberg( 1999 ) Focardi, R., Martinelli, F.: A uniform approach for the definition of security properties. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM'99 -- Formal Methods. pp. 794--813. Springer Berlin Heidelberg, Berlin, Heidelberg(1999)"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3046679"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.1982.10014"},{"key":"e_1_3_2_1_18_1","volume-title":"Buckley","author":"Gosling J.","year":"2014","unstructured":"Gosling , J. , Joy , B. , Steele , G.L. , Bracha , G. , Buckley , A. : The Java Language Specification, Java SE 8 Edition. Addison-Wesley Professional , 1 st edn. ( 2014 ) Gosling, J., Joy, B., Steele, G.L., Bracha, G., Buckley, A.: The Java Language Specification, Java SE 8 Edition. Addison-Wesley Professional, 1st edn. (2014)","edition":"1"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1594834.1480898"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2005.02.006"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2362389.2362393"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/317636.317785"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511813672","volume-title":"Programming in Haskell","author":"Hutton G.","year":"2007","unstructured":"Hutton , G. : Programming in Haskell . Cambridge University Press , New York, NY, USA ( 2007 ) Hutton, G.: Programming in Haskell. Cambridge University Press, New York, NY, USA (2007)"},{"key":"e_1_3_2_1_24_1","first-page":"291","volume-title":"Yen","author":"Joye M.","year":"2002","unstructured":"Joye , M. , Yen , S.M. : The montgomery powering ladder. In : Kaliski, B.S., Ko\u00e7, \u00e7.K., Paar, C. (eds.) Cryptographic Hardware and Embedded Systems - CHES 2002 . pp. 291 -- 302 . Springer Berlin Heidelberg , Berlin, Heidelberg (2003) Joye, M., Yen, S.M.: The montgomery powering ladder. In: Kaliski, B.S., Ko\u00e7, \u00e7.K., Paar, C. (eds.) Cryptographic Hardware and Embedded Systems - CHES 2002. pp. 291--302. Springer Berlin Heidelberg, Berlin, Heidelberg (2003)"},{"key":"e_1_3_2_1_25_1","first-page":"1","volume-title":"Ferdinand","author":"K\u00e4stner D.","year":"2019","unstructured":"K\u00e4stner , D. , Pister , M. , Wegener , S. , Ferdinand , C. : TimeWeaver: A Tool for Hybrid Worst-Case Execution Time Analysis. In : Altmeyer, S. (ed.) 19th International Workshop on Worst-Case Execution Time Analysis (WCET 2019 ). OpenAccess Series in Informatics (OASIcs), vol. 72 , pp. 1: 1 -- 1.11 . Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany ( 2019). https:\/\/doi.org\/10.4230\/OASIcs.WCET.2019.1, http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2019\/10766 10.4230\/OASIcs.WCET.2019.1 K\u00e4stner, D., Pister, M., Wegener, S., Ferdinand, C.: TimeWeaver: A Tool for Hybrid Worst-Case Execution Time Analysis. In: Altmeyer, S. (ed.) 19th International Workshop on Worst-Case Execution Time Analysis (WCET 2019). OpenAccess Series in Informatics (OASIcs), vol. 72, pp. 1:1--1.11. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2019). https:\/\/doi.org\/10.4230\/OASIcs.WCET.2019.1, http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2019\/10766"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2700104"},{"key":"e_1_3_2_1_27_1","first-page":"388","volume-title":"Jun","author":"Kocher P.","year":"1999","unstructured":"Kocher , P. , Jaffe , J. , Jun , B. : Differential power analysis. In : Wiener, M. (ed.) Advances in Cryptology -- CRYPTO' 99. pp. 388 -- 397 . Springer Berlin Heidelberg , Berlin, Heidelberg ( 1999 ) Kocher, P., Jaffe, J., Jun, B.: Differential power analysis. In: Wiener, M. (ed.) Advances in Cryptology -- CRYPTO' 99. pp. 388--397. Springer Berlin Heidelberg, Berlin, Heidelberg (1999)"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"crossref","first-page":"104","DOI":"10.1007\/3-540-68697-5_9","volume-title":"Advances in Cryptology -- CRYPTO '96.","author":"Kocher P.C.","year":"1996","unstructured":"Kocher , P.C. : Timing attacks on implementations of diffie-hellman, rsa, dss, and other systems . In: Koblitz, N. (ed.) Advances in Cryptology -- CRYPTO '96. pp. 104 -- 113 . Springer Berlin Heidelberg , Berlin, Heidelberg ( 1996 ) Kocher, P.C.: Timing attacks on implementations of diffie-hellman, rsa, dss, and other systems. In: Koblitz, N. (ed.) Advances in Cryptology -- CRYPTO '96. pp. 104--113. Springer Berlin Heidelberg, Berlin, Heidelberg (1996)"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167132.3167336"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429090"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/43.664229"},{"key":"e_1_3_2_1_32_1","first-page":"72","volume-title":"Eder","author":"Liqat U.","year":"2013","unstructured":"Liqat , U. , Kerrison , S. , Serrano , A. , Georgiou , K. , L\u00f3pez-Garc\u00eda , P. , Grech , N. , Hermenegildo , M.V. , Eder , K. : Energy consumption analysis of programs based on XMOS isa-level models. In : LOPSTR. Lecture Notes in Computer Science, vol. 8901 , pp. 72 -- 90 . Springer ( 2013 ) Liqat, U., Kerrison, S., Serrano, A., Georgiou, K., L\u00f3pez-Garc\u00eda, P., Grech, N., Hermenegildo, M.V., Eder, K.: Energy consumption analysis of programs based on XMOS isa-level models. In: LOPSTR. Lecture Notes in Computer Science, vol. 8901, pp. 72--90. Springer (2013)"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068418000042"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3173042"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263712"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.micpro.2012.12.004"},{"key":"e_1_3_2_1_37_1","volume-title":"Bennett","author":"Pallister J.","year":"2013","unstructured":"Pallister , J. , Hollis , S.J. , Bennett , J. : BEEBS: open benchmarks for energy measurements on embedded platforms. CoRR abs\/1308.5174 ( 2013 ), http:\/\/arxiv.org\/abs\/1308.5174 Pallister, J., Hollis, S.J., Bennett, J.: BEEBS: open benchmarks for energy measurements on embedded platforms. CoRR abs\/1308.5174 (2013), http:\/\/arxiv.org\/abs\/1308.5174"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.23919\/DATE.2017.7927267"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/359340.359342"},{"key":"e_1_3_2_1_40_1","first-page":"1","volume-title":"International School on Foundations of Security Analysis and Design.","author":"Ryan P.Y.","year":"2000","unstructured":"Ryan , P.Y. : Mathematical models of computer security . In: International School on Foundations of Security Analysis and Design. pp. 1 -- 62 . Springer ( 2000 ) Ryan, P.Y.: Mathematical models of computer security. In: International School on Foundations of Security Analysis and Design. pp. 1--62. Springer (2000)"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1017\/S147106841400057X"},{"key":"e_1_3_2_1_42_1","first-page":"389","volume-title":"Brooks","author":"Shao Y.S.","year":"2013","unstructured":"Shao , Y.S. , Brooks , D.M. : Energy characterization and instruction-level energy model of intel's xeon phi processor. In : ISLPED. pp. 389 -- 394 . IEEE ( 2013 ) Shao, Y.S., Brooks, D.M.: Energy characterization and instruction-level energy model of intel's xeon phi processor. In: ISLPED. pp. 389--394. IEEE (2013)"},{"key":"e_1_3_2_1_44_1","first-page":"40","volume-title":"CICM 2017, Edinburgh, UK, July 17-21, 2017, Proceedings.","author":"Slama F.","year":"2017","unstructured":"Slama , F. , Brady , E. : Automatically proving equivalence by type-safe reflection. In: Intelligent Computer Mathematics - 10th International Conference , CICM 2017, Edinburgh, UK, July 17-21, 2017, Proceedings. pp. 40 -- 55 ( 2017 ). https:\/\/doi.org\/10.1007\/978-3-319-62075-6_4, https:\/\/doi.org\/10.1007\/978-3-319-62075-6_4 10.1007\/978-3-319-62075-6_4 Slama, F., Brady, E.: Automatically proving equivalence by type-safe reflection. In: Intelligent Computer Mathematics - 10th International Conference, CICM 2017, Edinburgh, UK, July 17-21, 2017, Proceedings. pp. 40--55 (2017). https:\/\/doi.org\/10.1007\/978-3-319-62075-6_4, https:\/\/doi.org\/10.1007\/978-3-319-62075-6_4"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2008.29"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/92.335012"},{"key":"e_1_3_2_1_47_1","first-page":"86","volume-title":"15th International Workshop, IFL 2003","author":"Vasconcelos P.B.","year":"2003","unstructured":"Vasconcelos , P.B. , Hammond , K. : Inferring cost equations for recursive, polymorphic and higher-order functional programs. In: Implementation of Functional Languages , 15th International Workshop, IFL 2003 , Edinburgh, UK , September 8-11, 2003 , Revised Papers. pp. 86 -- 101 (2003). https:\/\/doi.org\/10.1007\/978-3-540-27861-0_6, https:\/\/doi.org\/10.1007\/978-3-540-27861-0_6 10.1007\/978-3-540-27861-0_6 Vasconcelos, P.B., Hammond, K.: Inferring cost equations for recursive, polymorphic and higher-order functional programs. In: Implementation of Functional Languages, 15th International Workshop, IFL 2003, Edinburgh, UK, September 8-11, 2003, Revised Papers. pp. 86--101 (2003). https:\/\/doi.org\/10.1007\/978-3-540-27861-0_6, https:\/\/doi.org\/10.1007\/978-3-540-27861-0_6"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-1996-42-304"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/1347375.1347389"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/1347375.1347389"},{"key":"e_1_3_2_1_51_1","first-page":"664","volume-title":"Li","author":"Xian C.","year":"2007","unstructured":"Xian , C. , Lu , Y. , Li , Z. : Energy-aware scheduling for real-time multiprocessor systems with uncertain task execution time. In : DAC. pp. 664 -- 669 . IEEE ( 2007 ) Xian, C., Lu, Y., Li, Z.: Energy-aware scheduling for real-time multiprocessor systems with uncertain task execution time. In: DAC. pp. 664--669. IEEE (2007)"},{"volume-title":"R.: A survey on fault injection techniques. International Arab Journal of Information Technology","author":"Ziade H.","key":"e_1_3_2_1_52_1","unstructured":"Ziade , H. , Ayoubi , R. , Velazco , R.: A survey on fault injection techniques. International Arab Journal of Information Technology Vol. 1 , No. 2, July, 171--186 (2004), https:\/\/hal.archives-ouvertes.fr\/hal-00105562 Ziade, H., Ayoubi, R., Velazco, R.: A survey on fault injection techniques. International Arab Journal of Information Technology Vol. 1, No. 2, July, 171--186 (2004), https:\/\/hal.archives-ouvertes.fr\/hal-00105562"}],"event":{"name":"PPDP '19: Principles and Practice of Programming Languages 2019","sponsor":["Sony Sony Corporation"],"location":"Porto Portugal","acronym":"PPDP '19"},"container-title":["Proceedings of the 21st International Symposium on Principles and Practice of Declarative Programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3354166.3354171","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3354166.3354171","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:44:56Z","timestamp":1750203896000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3354166.3354171"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10,7]]},"references-count":51,"alternative-id":["10.1145\/3354166.3354171","10.1145\/3354166"],"URL":"https:\/\/doi.org\/10.1145\/3354166.3354171","relation":{},"subject":[],"published":{"date-parts":[[2019,10,7]]},"assertion":[{"value":"2019-10-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}