{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:36:23Z","timestamp":1750221383904,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":24,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,12,25]],"date-time":"2017-12-25T00:00:00Z","timestamp":1514160000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/K035584\/1"],"award-info":[{"award-number":["EP\/K035584\/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":[[2017,12,25]]},"DOI":"10.1145\/3162071","type":"proceedings-article","created":{"date-parts":[[2018,6,1]],"date-time":"2018-06-01T20:20:41Z","timestamp":1527884441000},"page":"53-59","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Checking cryptographic API usage with composable annotations (short paper)"],"prefix":"10.1145","author":[{"given":"Duncan","family":"Mitchell","sequence":"first","affiliation":[{"name":"Royal Holloway University of London, UK"}]},{"given":"L. Thomas","family":"van Binsbergen","sequence":"additional","affiliation":[{"name":"Royal Holloway University of London, UK"}]},{"given":"Blake","family":"Loring","sequence":"additional","affiliation":[{"name":"Royal Holloway University of London, UK"}]},{"given":"Johannes","family":"Kinder","sequence":"additional","affiliation":[{"name":"Royal Holloway University of London, UK"}]}],"member":"320","published-online":{"date-parts":[[2017,12,25]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"What's wrong with in-browser cryptography? https:\/\/tonyarcieri.com\/whats-wrong-with-webcrypto (Last accessed","author":"Arcieri Tony","year":"2017","unstructured":"Tony Arcieri . 2013. What's wrong with in-browser cryptography? https:\/\/tonyarcieri.com\/whats-wrong-with-webcrypto (Last accessed : 22 November 2017 ). Tony Arcieri. 2013. What's wrong with in-browser cryptography? https:\/\/tonyarcieri.com\/whats-wrong-with-webcrypto (Last accessed: 22 November 2017)."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1890028.1890031"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2017.26"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"crossref","unstructured":"Karthikeyan Bhargavan Antoine Delignat-Lavaud and Sergio Maffeis. 2014. Defensive JavaScript - Building and Verifying Secure Web Components. In Foundations of Security Analysis and Design VII (FOSAD).  Karthikeyan Bhargavan Antoine Delignat-Lavaud and Sergio Maffeis. 2014. Defensive JavaScript - Building and Verifying Secure Web Components. In Foundations of Security Analysis and Design VII (FOSAD) .","DOI":"10.1007\/978-3-319-10082-1_4"},{"key":"e_1_3_2_1_5_1","volume-title":"Type-checking Higher-Order Security Libraries. In Asian Symp. on Programming Languages and Systems (APLAS).","author":"Bhargavan Karthikeyan","year":"2010","unstructured":"Karthikeyan Bhargavan , C\u00e9dric Fournet , and Nataliya Guts . 2010 . Type-checking Higher-Order Security Libraries. In Asian Symp. on Programming Languages and Systems (APLAS). Karthikeyan Bhargavan, C\u00e9dric Fournet, and Nataliya Guts. 2010. Type-checking Higher-Order Security Libraries. In Asian Symp. on Programming Languages and Systems (APLAS)."},{"key":"e_1_3_2_1_6_1","volume-title":"Implementing TLS with Verified Cryptographic Security. In IEEE Symp. on Security and Privacy (S&P).","author":"Bhargavan Karthikeyan","year":"2013","unstructured":"Karthikeyan Bhargavan , C\u00e9dric Fournet , Markulf Kohlweiss , Alfredo Pironti , and Pierre-Yves Strub . 2013 . Implementing TLS with Verified Cryptographic Security. In IEEE Symp. on Security and Privacy (S&P). Karthikeyan Bhargavan, C\u00e9dric Fournet, Markulf Kohlweiss, Alfredo Pironti, and Pierre-Yves Strub. 2013. Implementing TLS with Verified Cryptographic Security. In IEEE Symp. on Security and Privacy (S&P)."},{"key":"e_1_3_2_1_7_1","volume-title":"Dependent Types for JavaScript. In ACM SIGPLAN Conf. on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA).","author":"Chugh Ravi","year":"2012","unstructured":"Ravi Chugh , David Herman , and Ranjit Jhala . 2012 . Dependent Types for JavaScript. In ACM SIGPLAN Conf. on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA). Ravi Chugh, David Herman, and Ranjit Jhala. 2012. Dependent Types for JavaScript. In ACM SIGPLAN Conf. on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA)."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/301618.301665"},{"key":"e_1_3_2_1_9_1","volume-title":"Gordon","author":"Fournet C\u00e9dric","year":"2011","unstructured":"C\u00e9dric Fournet , Karthikeyan Bhargavan , and Andrew D . Gordon . 2011 . Cryptographic Verification by Typing for a Sample Protocol Implementation. In Foundations of Security Analysis and Design VI (FOSAD) . C\u00e9dric Fournet, Karthikeyan Bhargavan, and Andrew D. Gordon. 2011. Cryptographic Verification by Typing for a Sample Protocol Implementation. In Foundations of Security Analysis and Design VI (FOSAD)."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103663"},{"key":"e_1_3_2_1_11_1","volume-title":"The Essence of JavaScript. In European Conf. on Object-Oriented Programming (ECOOP).","author":"Guha Arjun","year":"2010","unstructured":"Arjun Guha , Claudiu Saftoiu , and Shriram Krishnamurthi . 2010 . The Essence of JavaScript. In European Conf. on Object-Oriented Programming (ECOOP). Arjun Guha, Claudiu Saftoiu, and Shriram Krishnamurthi. 2010. The Essence of JavaScript. In European Conf. on Object-Oriented Programming (ECOOP)."},{"key":"e_1_3_2_1_12_1","volume-title":"IEEE Symp. on Security and Privacy (S&P).","author":"Jovanovic Nenad","year":"2006","unstructured":"Nenad Jovanovic , Christopher Kr\u00fcgel , and Engin Kirda . 2006 . Pixy: A Static Analysis Tool for Detecting Web Application Vulnerabilities (Short Paper) . In IEEE Symp. on Security and Privacy (S&P). Nenad Jovanovic, Christopher Kr\u00fcgel, and Engin Kirda. 2006. Pixy: A Static Analysis Tool for Detecting Web Application Vulnerabilities (Short Paper). In IEEE Symp. on Security and Privacy (S&P)."},{"key":"e_1_3_2_1_13_1","volume-title":"TreatJS: Higher-Order Contracts for JavaScripts. In European Conf. on Object-Oriented Programming (ECOOP).","author":"Keil Matthias","year":"2015","unstructured":"Matthias Keil and Peter Thiemann . 2015 . TreatJS: Higher-Order Contracts for JavaScripts. In European Conf. on Object-Oriented Programming (ECOOP). Matthias Keil and Peter Thiemann. 2015. TreatJS: Higher-Order Contracts for JavaScripts. In European Conf. on Object-Oriented Programming (ECOOP)."},{"key":"e_1_3_2_1_14_1","volume-title":"Automated Verification for Secure Messaging Protocols and Their Implementations: A Symbolic and Computational Approach. In IEEE European Symp. on Security and Privacy (EuroS&P).","author":"Kobeissi Nadim","year":"2017","unstructured":"Nadim Kobeissi , Karthikeyan Bhargavan , and Bruno Blanchet . 2017 . Automated Verification for Secure Messaging Protocols and Their Implementations: A Symbolic and Computational Approach. In IEEE European Symp. on Security and Privacy (EuroS&P). Nadim Kobeissi, Karthikeyan Bhargavan, and Bruno Blanchet. 2017. Automated Verification for Secure Messaging Protocols and Their Implementations: A Symbolic and Computational Approach. In IEEE European Symp. on Security and Privacy (EuroS&P)."},{"volume-title":"Types and Programming Languages","author":"Pierce Benjamin C.","key":"e_1_3_2_1_15_1","unstructured":"Benjamin C. Pierce . 2002. Types and Programming Languages . MIT Press . Benjamin C. Pierce. 2002. Types and Programming Languages. MIT Press."},{"key":"e_1_3_2_1_16_1","volume-title":"JavaScript Cryptography Considered Harmful. https:\/\/www.nccgroup.trust\/us\/about-us\/newsroom-and-events\/blog\/2011\/august\/javascript-cryptography-considered-harmful\/ (Last accessed","author":"Ptacek Thomas","year":"2017","unstructured":"Thomas Ptacek . 2011. JavaScript Cryptography Considered Harmful. https:\/\/www.nccgroup.trust\/us\/about-us\/newsroom-and-events\/blog\/2011\/august\/javascript-cryptography-considered-harmful\/ (Last accessed : 22 November 2017 ). Thomas Ptacek. 2011. JavaScript Cryptography Considered Harmful. https:\/\/www.nccgroup.trust\/us\/about-us\/newsroom-and-events\/blog\/2011\/august\/javascript-cryptography-considered-harmful\/ (Last accessed: 22 November 2017)."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2002.806121"},{"key":"e_1_3_2_1_18_1","volume-title":"Towards Logic-Based Verification of JavaScript Programs. In Int. Conf. on Automated Deduction (CADE).","author":"Santos Jos\u00e9 Fragoso","year":"2017","unstructured":"Jos\u00e9 Fragoso Santos , Philippa Gardner , Petar Maksimovic , and Daiva Naudziuniene . 2017 . Towards Logic-Based Verification of JavaScript Programs. In Int. Conf. on Automated Deduction (CADE). Jos\u00e9 Fragoso Santos, Philippa Gardner, Petar Maksimovic, and Daiva Naudziuniene. 2017. Towards Logic-Based Verification of JavaScript Programs. In Int. Conf. on Automated Deduction (CADE)."},{"key":"e_1_3_2_1_19_1","unstructured":"Koushik Sen Swaroop Kalasapur Tasneem G. Brutch and Simon Gibbs. 2013. Jalangi: A Selective Record-Replay and Dynamic Analysis Framework for JavaScript. In Joint Meeting of the European Software Engineering Conf. and the ACM SIGSOFT Symp. on the Foundations of Software Engineering (ESEC\/FSE).   Koushik Sen Swaroop Kalasapur Tasneem G. Brutch and Simon Gibbs. 2013. Jalangi: A Selective Record-Replay and Dynamic Analysis Framework for JavaScript. In Joint Meeting of the European Software Engineering Conf. and the ACM SIGSOFT Symp. on the Foundations of Software Engineering (ESEC\/FSE) ."},{"key":"e_1_3_2_1_20_1","volume-title":"Secure Distributed Programming with Value-Dependent Types. In ACM SIGPLAN Int. Conf. on Functional Programming (ICFP).","author":"Swamy Nikhil","year":"2011","unstructured":"Nikhil Swamy , Juan Chen , C\u00e9dric Fournet , Pierre-Yves Strub , Karthikeyan Bhargavan , and Jean Yang . 2011 . Secure Distributed Programming with Value-Dependent Types. In ACM SIGPLAN Int. Conf. on Functional Programming (ICFP). Nikhil Swamy, Juan Chen, C\u00e9dric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, and Jean Yang. 2011. Secure Distributed Programming with Value-Dependent Types. In ACM SIGPLAN Int. Conf. on Functional Programming (ICFP)."},{"key":"e_1_3_2_1_21_1","volume-title":"Automated Analysis of Security-Critical JavaScript APIs. In IEEE Symp. on Security and Privacy (S&P).","author":"Taly Ankur","year":"2011","unstructured":"Ankur Taly , \u00dalfar Erlingsson , John C. Mitchell , Mark S. Miller , and Jasvir Nagra . 2011 . Automated Analysis of Security-Critical JavaScript APIs. In IEEE Symp. on Security and Privacy (S&P). Ankur Taly, \u00dalfar Erlingsson, John C. Mitchell, Mark S. Miller, and Jasvir Nagra. 2011. Automated Analysis of Security-Critical JavaScript APIs. In IEEE Symp. on Security and Privacy (S&P)."},{"key":"e_1_3_2_1_22_1","volume-title":"https:\/\/tobtu.com\/decryptocat.php (Last accessed","author":"Thomas Steve","year":"2017","unstructured":"Steve Thomas . 2013. Decryptocat. https:\/\/tobtu.com\/decryptocat.php (Last accessed : 22 November 2017 ). Steve Thomas. 2013. Decryptocat. https:\/\/tobtu.com\/decryptocat.php (Last accessed: 22 November 2017)."},{"key":"e_1_3_2_1_23_1","volume-title":"Refinement Types for TypeScript. In ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI).","author":"Vekris Panagiotis","year":"2016","unstructured":"Panagiotis Vekris , Benjamin Cosman , and Ranjit Jhala . 2016 . Refinement Types for TypeScript. In ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI). Panagiotis Vekris, Benjamin Cosman, and Ranjit Jhala. 2016. Refinement Types for TypeScript. In ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI)."},{"key":"e_1_3_2_1_24_1","unstructured":"Mark Watson. 2017. Web Cryptography API. W3C Recommendation. W3C. https:\/\/www.w3.org\/TR\/2017\/REC-WebCryptoAPI-20170126\/.  Mark Watson. 2017. Web Cryptography API . W3C Recommendation. W3C. https:\/\/www.w3.org\/TR\/2017\/REC-WebCryptoAPI-20170126\/."}],"event":{"name":"POPL '18: The 45th Annual ACM SIGPLAN Symposium on Principles of Programming Languages","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"],"location":"Los Angeles CA USA","acronym":"POPL '18"},"container-title":["Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3162071","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3162071","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:26:54Z","timestamp":1750213614000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3162071"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,25]]},"references-count":24,"alternative-id":["10.1145\/3162071","10.1145\/3175493"],"URL":"https:\/\/doi.org\/10.1145\/3162071","relation":{},"subject":[],"published":{"date-parts":[[2017,12,25]]},"assertion":[{"value":"2017-12-25","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}