{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:08:29Z","timestamp":1750219709285,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":37,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,10,22]],"date-time":"2023-10-22T00:00:00Z","timestamp":1697932800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["ANR-18-CE25-0014"],"award-info":[{"award-number":["ANR-18-CE25-0014"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,10,22]]},"DOI":"10.1145\/3610612.3610618","type":"proceedings-article","created":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T23:13:48Z","timestamp":1697498028000},"page":"1-13","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Type-directed Program Transformation for Constant-Time Enforcement"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0006-7136-8592","authenticated-orcid":false,"given":"Gautier","family":"Raimondi","sequence":"first","affiliation":[{"name":"Inria, Univ. Rennes, CNRS, IRISA, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6815-0652","authenticated-orcid":false,"given":"Fr\u00e9d\u00e9ric","family":"Besson","sequence":"additional","affiliation":[{"name":"Inria, Univ. Rennes, CNRS, IRISA, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4064-7170","authenticated-orcid":false,"given":"Thomas","family":"Jensen","sequence":"additional","affiliation":[{"name":"Inria, Univ. Rennes, CNRS, IRISA, France and University of Copenhagen, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,10,22]]},"reference":[{"volume-title":"Transforming Out Timing Leaks","author":"Agat Johan","key":"e_1_3_2_1_1_1","unstructured":"Johan Agat . 2000. Transforming Out Timing Leaks . In POPL, Mark\u00a0N. Wegman and Thomas\u00a0W. Reps (Eds.). ACM , 40\u201353. https:\/\/doi.org\/10.1145\/325694.325702 10.1145\/325694.325702 Johan Agat. 2000. Transforming Out Timing Leaks. In POPL, Mark\u00a0N. Wegman and Thomas\u00a0W. Reps (Eds.). ACM, 40\u201353. https:\/\/doi.org\/10.1145\/325694.325702"},{"volume-title":"Conversion of Control Dependence to Data Dependence","author":"Allen R.","key":"e_1_3_2_1_2_1","unstructured":"John\u00a0 R. Allen , Ken Kennedy , Carrie Porterfield , and Joe\u00a0 D. Warren . 1983. Conversion of Control Dependence to Data Dependence . In POPL, John\u00a0R. Wright, Larry Landweber, Alan\u00a0J. Demers, and Tim Teitelbaum (Eds.). ACM Press , 177\u2013189. https:\/\/doi.org\/10.1145\/567067.567085 10.1145\/567067.567085 John\u00a0R. Allen, Ken Kennedy, Carrie Porterfield, and Joe\u00a0D. Warren. 1983. Conversion of Control Dependence to Data Dependence. In POPL, John\u00a0R. Wright, Larry Landweber, Alan\u00a0J. Demers, and Tim Teitelbaum (Eds.). ACM Press, 177\u2013189. https:\/\/doi.org\/10.1145\/567067.567085"},{"key":"e_1_3_2_1_3_1","volume-title":"ACM","author":"Almeida Jos\u00e9\u00a0Bacelar","year":"2017","unstructured":"Jos\u00e9\u00a0Bacelar Almeida , Manuel Barbosa , Gilles Barthe , Arthur Blot , Benjamin Gr\u00e9goire , Vincent Laporte , Tiago Oliveira , Hugo Pacheco , Benedikt Schmidt , and Pierre-Yves Strub . 2017 . Jasmin: High-Assurance and High-Speed Cryptography. In CCS, Bhavani\u00a0M. Thuraisingham, David Evans, Tal Malkin, and Dongyan Xu (Eds.) . ACM , 1807\u20131823. https:\/\/doi.org\/10.1145\/3133956.3134078 10.1145\/3133956.3134078 Jos\u00e9\u00a0Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Arthur Blot, Benjamin Gr\u00e9goire, Vincent Laporte, Tiago Oliveira, Hugo Pacheco, Benedikt Schmidt, and Pierre-Yves Strub. 2017. Jasmin: High-Assurance and High-Speed Cryptography. In CCS, Bhavani\u00a0M. Thuraisingham, David Evans, Tal Malkin, and Dongyan Xu (Eds.). ACM, 1807\u20131823. https:\/\/doi.org\/10.1145\/3133956.3134078"},{"key":"e_1_3_2_1_4_1","volume-title":"Verifying Constant-Time Implementations. In 25th USENIX Security Symposium, Thorsten Holz and Stefan Savage (Eds.). USENIX Association, 53\u201370","author":"Almeida Jos\u00e9\u00a0Bacelar","year":"2016","unstructured":"Jos\u00e9\u00a0Bacelar Almeida , Manuel Barbosa , Gilles Barthe , Fran\u00e7ois Dupressoir , and Michael Emmi . 2016 . Verifying Constant-Time Implementations. In 25th USENIX Security Symposium, Thorsten Holz and Stefan Savage (Eds.). USENIX Association, 53\u201370 . https:\/\/www.usenix.org\/conference\/usenixsecurity16\/technical-sessions\/presentation\/almeida Jos\u00e9\u00a0Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Fran\u00e7ois Dupressoir, and Michael Emmi. 2016. Verifying Constant-Time Implementations. In 25th USENIX Security Symposium, Thorsten Holz and Stefan Savage (Eds.). USENIX Association, 53\u201370. https:\/\/www.usenix.org\/conference\/usenixsecurity16\/technical-sessions\/presentation\/almeida"},{"key":"e_1_3_2_1_5_1","volume-title":"S&P","author":"Almeida Jos\u00e9\u00a0Bacelar","year":"2020","unstructured":"Jos\u00e9\u00a0Bacelar Almeida , Manuel Barbosa , Gilles Barthe , Benjamin Gr\u00e9goire , Adrien Koutsos , Vincent Laporte , Tiago Oliveira , and Pierre-Yves Strub . 2020. The Last Mile: High-Assurance and High-Speed Cryptographic Implementations . In S&P . IEEE , 965\u2013982. https:\/\/doi.org\/10.1109\/SP40000. 2020 .00028 10.1109\/SP40000.2020.00028 Jos\u00e9\u00a0Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Gr\u00e9goire, Adrien Koutsos, Vincent Laporte, Tiago Oliveira, and Pierre-Yves Strub. 2020. The Last Mile: High-Assurance and High-Speed Cryptographic Implementations. In S&P. IEEE, 965\u2013982. https:\/\/doi.org\/10.1109\/SP40000.2020.00028"},{"key":"e_1_3_2_1_6_1","unstructured":"Jean-Philippe Aumasson 2020. Cryptocoding. https:\/\/github.com\/veorq\/cryptocoding  Jean-Philippe Aumasson 2020. Cryptocoding. https:\/\/github.com\/veorq\/cryptocoding"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9441-5"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-020-09548-x"},{"key":"#cr-split#-e_1_3_2_1_9_1.1","doi-asserted-by":"crossref","unstructured":"Gilles Barthe Gustavo Betarte Juan\u00a0Diego Campo Carlos\u00a0Daniel Luna and David Pichardie. 2014. System-level Non-interference for Constant-time Cryptography. In CCS Gail-Joon Ahn Moti Yung and Ninghui Li (Eds.). ACM 1267-1279. https:\/\/doi.org\/10.1145\/2660267.2660283 10.1145\/2660267.2660283","DOI":"10.1145\/2660267.2660283"},{"key":"#cr-split#-e_1_3_2_1_9_1.2","doi-asserted-by":"crossref","unstructured":"Gilles Barthe Gustavo Betarte Juan\u00a0Diego Campo Carlos\u00a0Daniel Luna and David Pichardie. 2014. System-level Non-interference for Constant-time Cryptography. In CCS Gail-Joon Ahn Moti Yung and Ninghui Li (Eds.). ACM 1267-1279. https:\/\/doi.org\/10.1145\/2660267.2660283","DOI":"10.1145\/2660267.2660283"},{"key":"e_1_3_2_1_10_1","volume-title":"Proc. ACM Program. Lang. 4, POPL","author":"Barthe Gilles","year":"2020","unstructured":"Gilles Barthe , Sandrine Blazy , Benjamin Gr\u00e9goire , R\u00e9mi Hutin , Vincent Laporte , David Pichardie , and Alix Trieu . 2020 . Formal verification of a constant-time preserving C compiler . Proc. ACM Program. Lang. 4, POPL (2020), 7:1\u20137:30. https:\/\/doi.org\/10.1145\/3371075 10.1145\/3371075 Gilles Barthe, Sandrine Blazy, Benjamin Gr\u00e9goire, R\u00e9mi Hutin, Vincent Laporte, David Pichardie, and Alix Trieu. 2020. Formal verification of a constant-time preserving C compiler. Proc. ACM Program. Lang. 4, POPL (2020), 7:1\u20137:30. https:\/\/doi.org\/10.1145\/3371075"},{"volume-title":"FOSAD Tutorial Lectures(LNCS, Vol.\u00a08604), Alessandro Aldini, Javier L\u00f3pez","author":"Barthe Gilles","key":"e_1_3_2_1_11_1","unstructured":"Gilles Barthe , Fran\u00e7ois Dupressoir , Benjamin Gr\u00e9goire , C\u00e9sar Kunz , Benedikt Schmidt , and Pierre-Yves Strub . 2013. EasyCrypt: A Tutorial . In FOSAD Tutorial Lectures(LNCS, Vol.\u00a08604), Alessandro Aldini, Javier L\u00f3pez , and Fabio Martinelli (Eds.). Springer , 146\u2013166. https:\/\/doi.org\/10.1007\/978-3-319-10082-1_6 10.1007\/978-3-319-10082-1_6 Gilles Barthe, Fran\u00e7ois Dupressoir, Benjamin Gr\u00e9goire, C\u00e9sar Kunz, Benedikt Schmidt, and Pierre-Yves Strub. 2013. EasyCrypt: A Tutorial. In FOSAD Tutorial Lectures(LNCS, Vol.\u00a08604), Alessandro Aldini, Javier L\u00f3pez, and Fabio Martinelli (Eds.). Springer, 146\u2013166. https:\/\/doi.org\/10.1007\/978-3-319-10082-1_6"},{"key":"e_1_3_2_1_12_1","volume-title":"Secure Compilation of Side-Channel Countermeasures: The Case of Cryptographic \"Constant-Time","author":"Barthe Gilles","year":"2018","unstructured":"Gilles Barthe , Benjamin Gr\u00e9goire , and Vincent Laporte . 2018. Secure Compilation of Side-Channel Countermeasures: The Case of Cryptographic \"Constant-Time \". In CSF. IEEE Computer Society , 328\u2013343. https:\/\/doi.org\/10.1109\/CSF. 2018 .00031 10.1109\/CSF.2018.00031 Gilles Barthe, Benjamin Gr\u00e9goire, and Vincent Laporte. 2018. Secure Compilation of Side-Channel Countermeasures: The Case of Cryptographic \"Constant-Time\". In CSF. IEEE Computer Society, 328\u2013343. https:\/\/doi.org\/10.1109\/CSF.2018.00031"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-181136"},{"key":"e_1_3_2_1_14_1","volume-title":"Vale: Verifying High-Performance Cryptographic Assembly Code","author":"Bond Barry","year":"2017","unstructured":"Barry Bond , Chris Hawblitzel , Manos Kapritsos , K.\u00a0Rustan\u00a0 M. Leino , Jacob\u00a0 R. Lorch , Bryan Parno , Ashay Rane , Srinath T.\u00a0V. Setty , and Laure Thompson . 2017 . Vale: Verifying High-Performance Cryptographic Assembly Code . In USENIX Security, Engin Kirda and Thomas Ristenpart (Eds.). USENIX Association , 917\u2013934. https:\/\/www.usenix.org\/conference\/usenixsecurity17\/technical-sessions\/presentation\/bond Barry Bond, Chris Hawblitzel, Manos Kapritsos, K.\u00a0Rustan\u00a0M. Leino, Jacob\u00a0R. Lorch, Bryan Parno, Ashay Rane, Srinath T.\u00a0V. Setty, and Laure Thompson. 2017. Vale: Verifying High-Performance Cryptographic Assembly Code. In USENIX Security, Engin Kirda and Thomas Ristenpart (Eds.). USENIX Association, 917\u2013934. https:\/\/www.usenix.org\/conference\/usenixsecurity17\/technical-sessions\/presentation\/bond"},{"key":"e_1_3_2_1_15_1","volume-title":"Constant-Time Programming Language","author":"Cauligi Sunjay","year":"2017","unstructured":"Sunjay Cauligi , Gary Soeller , Fraser Brown , Brian Johannesmeyer , Yunlu Huang , Ranjit Jhala , and Deian Stefan . 2017. FaCT : A Flexible , Constant-Time Programming Language . In IEEE Cybersecurity Development, Sec Dev 2017 . IEEE Computer Society , 69\u201376. https:\/\/doi.org\/10.1109\/SecDev.2017.24 10.1109\/SecDev.2017.24 Sunjay Cauligi, Gary Soeller, Fraser Brown, Brian Johannesmeyer, Yunlu Huang, Ranjit Jhala, and Deian Stefan. 2017. FaCT: A Flexible, Constant-Time Programming Language. In IEEE Cybersecurity Development, SecDev 2017. IEEE Computer Society, 69\u201376. https:\/\/doi.org\/10.1109\/SecDev.2017.24"},{"key":"#cr-split#-e_1_3_2_1_16_1.1","doi-asserted-by":"crossref","unstructured":"Sunjay Cauligi Gary Soeller Brian Johannesmeyer Fraser Brown Riad\u00a0S. Wahby John Renner Benjamin Gr\u00e9goire Gilles Barthe Ranjit Jhala and Deian Stefan. 2019. FaCT: a DSL for timing-sensitive computation. In PLDI Kathryn\u00a0S. McKinley and Kathleen Fisher (Eds.). ACM 174-189. https:\/\/doi.org\/10.1145\/3314221.3314605 10.1145\/3314221.3314605","DOI":"10.1145\/3314221.3314605"},{"key":"#cr-split#-e_1_3_2_1_16_1.2","doi-asserted-by":"crossref","unstructured":"Sunjay Cauligi Gary Soeller Brian Johannesmeyer Fraser Brown Riad\u00a0S. Wahby John Renner Benjamin Gr\u00e9goire Gilles Barthe Ranjit Jhala and Deian Stefan. 2019. FaCT: a DSL for timing-sensitive computation. In PLDI Kathryn\u00a0S. McKinley and Kathleen Fisher (Eds.). ACM 174-189. https:\/\/doi.org\/10.1145\/3314221.3314605","DOI":"10.1145\/3314221.3314605"},{"key":"e_1_3_2_1_17_1","volume-title":"Proc. ACM Program. Lang. 3, POPL","author":"Fromherz Aymeric","year":"2019","unstructured":"Aymeric Fromherz , Nick Giannarakis , Chris Hawblitzel , Bryan Parno , Aseem Rastogi , and Nikhil Swamy . 2019 . A verified, efficient embedding of a verifiable assembly language . Proc. ACM Program. Lang. 3, POPL (2019), 63:1\u201363:30. https:\/\/doi.org\/10.1145\/3290376 10.1145\/3290376 Aymeric Fromherz, Nick Giannarakis, Chris Hawblitzel, Bryan Parno, Aseem Rastogi, and Nikhil Swamy. 2019. A verified, efficient embedding of a verifiable assembly language. Proc. ACM Program. Lang. 3, POPL (2019), 63:1\u201363:30. https:\/\/doi.org\/10.1145\/3290376"},{"key":"#cr-split#-e_1_3_2_1_18_1.1","doi-asserted-by":"crossref","unstructured":"Sebastian Hunt and David Sands. 2006. On flow-sensitive security types. In POPL. ACM 79-90. https:\/\/doi.org\/10.1145\/1111037.1111045 10.1145\/1111037.1111045","DOI":"10.1145\/1111320.1111045"},{"key":"#cr-split#-e_1_3_2_1_18_1.2","doi-asserted-by":"crossref","unstructured":"Sebastian Hunt and David Sands. 2006. On flow-sensitive security types. In POPL. ACM 79-90. https:\/\/doi.org\/10.1145\/1111037.1111045","DOI":"10.1145\/1111320.1111045"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3399742"},{"key":"e_1_3_2_1_20_1","volume-title":"16th Annual International Cryptology Conference(LNCS, Vol.\u00a01109)","author":"Kocher C.","year":"1996","unstructured":"Paul\u00a0 C. Kocher . 1996 . Timing Attacks on Implementations of Diffie-Hellman, RSA, DSS, and Other Systems . In 16th Annual International Cryptology Conference(LNCS, Vol.\u00a01109) , Neal Koblitz (Ed.). Springer, 104\u2013113. https:\/\/doi.org\/10.1007\/3-540-68697-5_9 10.1007\/3-540-68697-5_9 Paul\u00a0C. Kocher. 1996. Timing Attacks on Implementations of Diffie-Hellman, RSA, DSS, and Other Systems. In 16th Annual International Cryptology Conference(LNCS, Vol.\u00a01109), Neal Koblitz (Ed.). Springer, 104\u2013113. https:\/\/doi.org\/10.1007\/3-540-68697-5_9"},{"key":"e_1_3_2_1_21_1","volume-title":"Dafny: An Automatic Program Verifier for Functional Correctness. In LPAR(LNCS, Vol.\u00a06355), Edmund\u00a0M","author":"Leino M.","year":"2010","unstructured":"K.\u00a0Rustan\u00a0 M. Leino . 2010 . Dafny: An Automatic Program Verifier for Functional Correctness. In LPAR(LNCS, Vol.\u00a06355), Edmund\u00a0M . Clarke and Andrei Voronkov (Eds.). Springer , 348\u2013370. https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20 10.1007\/978-3-642-17511-4_20 K.\u00a0Rustan\u00a0M. Leino. 2010. Dafny: An Automatic Program Verifier for Functional Correctness. In LPAR(LNCS, Vol.\u00a06355), Edmund\u00a0M. Clarke and Andrei Voronkov (Eds.). Springer, 348\u2013370. https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20"},{"key":"e_1_3_2_1_22_1","volume-title":"Memory Trace Oblivious Program Execution","author":"Liu Chang","year":"2013","unstructured":"Chang Liu , Michael Hicks , and Elaine Shi . 2013. Memory Trace Oblivious Program Execution . In CSF. IEEE Computer Society , 51\u201365. https:\/\/doi.org\/10.1109\/CSF. 2013 .11 10.1109\/CSF.2013.11 Chang Liu, Michael Hicks, and Elaine Shi. 2013. Memory Trace Oblivious Program Execution. In CSF. IEEE Computer Society, 51\u201365. https:\/\/doi.org\/10.1109\/CSF.2013.11"},{"volume-title":"More or Less. In ESORICS(LNCS, Vol.\u00a09326)","author":"Mantel Heiko","key":"e_1_3_2_1_23_1","unstructured":"Heiko Mantel and Artem Starostin . 2015. Transforming Out Timing Leaks , More or Less. In ESORICS(LNCS, Vol.\u00a09326) . Springer , 447\u2013467. Heiko Mantel and Artem Starostin. 2015. Transforming Out Timing Leaks, More or Less. In ESORICS(LNCS, Vol.\u00a09326). Springer, 447\u2013467."},{"volume-title":"ICISC(LNCS, Vol.\u00a03935)","author":"Molnar David","key":"e_1_3_2_1_24_1","unstructured":"David Molnar , Matt Piotrowski , David Schultz , and David\u00a0 A. Wagner . 2005. The Program Counter Security Model: Automatic Detection and Removal of Control-Flow Side Channel Attacks . In ICISC(LNCS, Vol.\u00a03935) , Dongho Won and Seungjoo Kim (Eds.). Springer , 156\u2013168. https:\/\/doi.org\/10.1007\/11734727_14 10.1007\/11734727_14 David Molnar, Matt Piotrowski, David Schultz, and David\u00a0A. Wagner. 2005. The Program Counter Security Model: Automatic Detection and Removal of Control-Flow Side Channel Attacks. In ICISC(LNCS, Vol.\u00a03935), Dongho Won and Seungjoo Kim (Eds.). Springer, 156\u2013168. https:\/\/doi.org\/10.1007\/11734727_14"},{"key":"e_1_3_2_1_25_1","volume-title":"Proc. ACM Program. Lang. 1, ICFP","author":"Protzenko Jonathan","year":"2017","unstructured":"Jonathan Protzenko , Jean\u00a0Karim Zinzindohou\u00e9 , Aseem Rastogi , Tahina Ramananandro , Peng Wang , Santiago\u00a0Zanella B\u00e9guelin , Antoine Delignat-Lavaud , Catalin Hritcu , Karthikeyan Bhargavan , C\u00e9dric Fournet , and Nikhil Swamy . 2017 . Verified low-level programming embedded in F . Proc. ACM Program. Lang. 1, ICFP (2017), 17:1\u201317:29. https:\/\/doi.org\/10.1145\/3110261 10.1145\/3110261 Jonathan Protzenko, Jean\u00a0Karim Zinzindohou\u00e9, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago\u00a0Zanella B\u00e9guelin, Antoine Delignat-Lavaud, Catalin Hritcu, Karthikeyan Bhargavan, C\u00e9dric Fournet, and Nikhil Swamy. 2017. Verified low-level programming embedded in F. Proc. ACM Program. Lang. 1, ICFP (2017), 17:1\u201317:29. https:\/\/doi.org\/10.1145\/3110261"},{"key":"e_1_3_2_1_26_1","unstructured":"Gautier Raimondi. 2023. Secure compilation against side-channel attacks. Ph.\u00a0D. Dissertation. Universit\u00e9 de Rennes.  Gautier Raimondi. 2023. Secure compilation against side-channel attacks. Ph.\u00a0D. Dissertation. Universit\u00e9 de Rennes."},{"key":"e_1_3_2_1_27_1","volume-title":"Fernando Magno\u00a0Quint\u00e3o Pereira, and Diego\u00a0F. Aranha","author":"Rodrigues Bruno","year":"2016","unstructured":"Bruno Rodrigues , Fernando Magno\u00a0Quint\u00e3o Pereira, and Diego\u00a0F. Aranha . 2016 . Sparse representation of implicit flows with applications to side-channel detection. In CC, Ayal Zaks and Manuel\u00a0V. Hermenegildo (Eds.). ACM , 110\u2013120. https:\/\/doi.org\/10.1145\/2892208.2892230 10.1145\/2892208.2892230 Bruno Rodrigues, Fernando Magno\u00a0Quint\u00e3o Pereira, and Diego\u00a0F. Aranha. 2016. Sparse representation of implicit flows with applications to side-channel detection. In CC, Ayal Zaks and Manuel\u00a0V. Hermenegildo (Eds.). ACM, 110\u2013120. https:\/\/doi.org\/10.1145\/2892208.2892230"},{"key":"e_1_3_2_1_28_1","volume-title":"Memory-Safe Elimination of Side Channels","author":"Soares Luigi","year":"2021","unstructured":"Luigi Soares and Fernando Magno\u00a0Quint\u00e3o Pereira . 2021. Memory-Safe Elimination of Side Channels . In IEEE\/ACM CGO, Jae\u00a0W. Lee, Mary\u00a0Lou Soffa, and Ayal Zaks (Eds.). IEEE , 200\u2013210. https:\/\/doi.org\/10.1109\/CGO51591. 2021 .9370305 10.1109\/CGO51591.2021.9370305 Luigi Soares and Fernando Magno\u00a0Quint\u00e3o Pereira. 2021. Memory-Safe Elimination of Side Channels. In IEEE\/ACM CGO, Jae\u00a0W. Lee, Mary\u00a0Lou Soffa, and Ayal Zaks (Eds.). IEEE, 200\u2013210. https:\/\/doi.org\/10.1109\/CGO51591.2021.9370305"},{"volume-title":"Dependent types and multi-monadic effects in F","author":"Swamy Nikhil","key":"e_1_3_2_1_29_1","unstructured":"Nikhil Swamy , Catalin Hritcu , Chantal Keller , Aseem Rastogi , Antoine Delignat-Lavaud , Simon Forest , Karthikeyan Bhargavan , C\u00e9dric Fournet , Pierre-Yves Strub , Markulf Kohlweiss , Jean\u00a0Karim Zinzindohoue , and Santiago\u00a0Zanella B\u00e9guelin . 2016. Dependent types and multi-monadic effects in F . In POPL, Rastislav Bod\u00edk and Rupak Majumdar (Eds.). ACM , 256\u2013270. https:\/\/doi.org\/10.1145\/2837614.2837655 10.1145\/2837614.2837655 Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, C\u00e9dric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean\u00a0Karim Zinzindohoue, and Santiago\u00a0Zanella B\u00e9guelin. 2016. Dependent types and multi-monadic effects in F. In POPL, Rastislav Bod\u00edk and Rupak Majumdar (Eds.). ACM, 256\u2013270. https:\/\/doi.org\/10.1145\/2837614.2837655"},{"key":"e_1_3_2_1_30_1","volume-title":"Proc. ACM Program. Lang. 5, POPL","author":"Vassena Marco","year":"2021","unstructured":"Marco Vassena , Craig Disselkoen , Klaus von Gleissenthall , Sunjay Cauligi , Rami\u00a0G\u00f6khan Kici , Ranjit Jhala , Dean\u00a0 M. Tullsen , and Deian Stefan . 2021 . Automatically eliminating speculative leaks from cryptographic code with blade . Proc. ACM Program. Lang. 5, POPL (2021), 1\u201330. https:\/\/doi.org\/10.1145\/3434330 10.1145\/3434330 Marco Vassena, Craig Disselkoen, Klaus von Gleissenthall, Sunjay Cauligi, Rami\u00a0G\u00f6khan Kici, Ranjit Jhala, Dean\u00a0M. Tullsen, and Deian Stefan. 2021. Automatically eliminating speculative leaks from cryptographic code with blade. Proc. ACM Program. Lang. 5, POPL (2021), 1\u201330. https:\/\/doi.org\/10.1145\/3434330"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/353629.353648"},{"volume-title":"Eliminating timing side-channel leaks using program repair","author":"Wu Meng","key":"e_1_3_2_1_32_1","unstructured":"Meng Wu , Shengjian Guo , Patrick Schaumont , and Chao Wang . 2018. Eliminating timing side-channel leaks using program repair . In ISSTA, Frank Tip and Eric Bodden (Eds.). ACM , 15\u201326. https:\/\/doi.org\/10.1145\/3213846.3213851 10.1145\/3213846.3213851 Meng Wu, Shengjian Guo, Patrick Schaumont, and Chao Wang. 2018. Eliminating timing side-channel leaks using program repair. In ISSTA, Frank Tip and Eric Bodden (Eds.). ACM, 15\u201326. https:\/\/doi.org\/10.1145\/3213846.3213851"},{"key":"#cr-split#-e_1_3_2_1_33_1.1","doi-asserted-by":"crossref","unstructured":"Jean\u00a0Karim Zinzindohou\u00e9 Karthikeyan Bhargavan Jonathan Protzenko and Benjamin Beurdouche. 2017. HACL*: A Verified Modern Cryptographic Library. In CCS Bhavani\u00a0M. Thuraisingham David Evans Tal Malkin and Dongyan Xu (Eds.). ACM 1789-1806. https:\/\/doi.org\/10.1145\/3133956.3134043 10.1145\/3133956.3134043","DOI":"10.1145\/3133956.3134043"},{"key":"#cr-split#-e_1_3_2_1_33_1.2","doi-asserted-by":"crossref","unstructured":"Jean\u00a0Karim Zinzindohou\u00e9 Karthikeyan Bhargavan Jonathan Protzenko and Benjamin Beurdouche. 2017. HACL*: A Verified Modern Cryptographic Library. In CCS Bhavani\u00a0M. Thuraisingham David Evans Tal Malkin and Dongyan Xu (Eds.). ACM 1789-1806. https:\/\/doi.org\/10.1145\/3133956.3134043","DOI":"10.1145\/3133956.3134043"}],"event":{"name":"PPDP 2023: International Symposium on Principles and Practice of Declarative Programming","acronym":"PPDP 2023","location":"Lisboa Portugal"},"container-title":["International Symposium on Principles and Practice of Declarative Programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3610612.3610618","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:36:00Z","timestamp":1750178160000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3610612.3610618"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,22]]},"references-count":37,"alternative-id":["10.1145\/3610612.3610618","10.1145\/3610612"],"URL":"https:\/\/doi.org\/10.1145\/3610612.3610618","relation":{},"subject":[],"published":{"date-parts":[[2023,10,22]]},"assertion":[{"value":"2023-10-22","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}