{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T20:40:32Z","timestamp":1759092032700,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":40,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,1,15]],"date-time":"2022-01-15T00:00:00Z","timestamp":1642204800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100010661","name":"Horizon 2020 Framework Programme","doi-asserted-by":"publisher","award":["779882"],"award-info":[{"award-number":["779882"]}],"id":[{"id":"10.13039\/100010661","id-type":"DOI","asserted-by":"publisher"}]},{"name":"EPSRC","award":["EP\/V006290\/1"],"award-info":[{"award-number":["EP\/V006290\/1"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,1,17]]},"DOI":"10.1145\/3498886.3502202","type":"proceedings-article","created":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T05:12:43Z","timestamp":1641964363000},"page":"14-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Semi-automatic ladderisation: improving code security through rewriting and dependent types"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6030-2885","authenticated-orcid":false,"given":"Christopher","family":"Brown","sequence":"first","affiliation":[{"name":"University of St. Andrews, UK"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1236-7160","authenticated-orcid":false,"given":"Adam D.","family":"Barwell","sequence":"additional","affiliation":[{"name":"University of St. Andrews, UK \/ Imperial College London, UK"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4607-967X","authenticated-orcid":false,"given":"Yoann","family":"Marquer","sequence":"additional","affiliation":[{"name":"Inria, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6830-2572","authenticated-orcid":false,"given":"Olivier","family":"Zendra","sequence":"additional","affiliation":[{"name":"Inria, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0189-4272","authenticated-orcid":false,"given":"Tania","family":"Richmond","sequence":"additional","affiliation":[{"name":"Inria, France \/ DGA, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7943-1468","authenticated-orcid":false,"given":"Chen","family":"Gu","sequence":"additional","affiliation":[{"name":"Hefei University of Technology, China"}]}],"member":"320","published-online":{"date-parts":[[2022,1,15]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"2013. Digital Signature Standard (DSS). https:\/\/nvlpubs.nist.gov\/nistpubs\/FIPS\/NIST.FIPS.186-4.pdf FIPS PUB 186-4 U.S.Department of Commerce\/National Institute of Standards and Technology.  2013. Digital Signature Standard (DSS). https:\/\/nvlpubs.nist.gov\/nistpubs\/FIPS\/NIST.FIPS.186-4.pdf FIPS PUB 186-4 U.S.Department of Commerce\/National Institute of Standards and Technology."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/tse.2020.3005995"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068410000487"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.6028\/NIST.SP.800-56Ar3"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3412932.3412944"},{"volume-title":"CRT RSA Algorithm Protected Against Fault Attacks","author":"Boscher Arnaud","key":"e_1_3_2_1_6_1","unstructured":"Arnaud Boscher , Robert Naciri , and Emmanuel Prouff . 2007. CRT RSA Algorithm Protected Against Fault Attacks . In Information Security Theory and Practices. Smart Cards, Mobile and Ubiquitous Computing Systems, Damien Sauveron, Konstantinos Markantonakis, Angelos Bilas, and Jean-Jacques Quisquater (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg . 229\u2013243. isbn:978-3-540-72354-7 Arnaud Boscher, Robert Naciri, and Emmanuel Prouff. 2007. CRT RSA Algorithm Protected Against Fault Attacks. In Information Security Theory and Practices. Smart Cards, Mobile and Ubiquitous Computing Systems, Damien Sauveron, Konstantinos Markantonakis, Angelos Bilas, and Jean-Jacques Quisquater (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 229\u2013243. isbn:978-3-540-72354-7"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681300018X"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.7494\/csci.2017.18.3.1413"},{"volume-title":"Type-Driven Development with Idris","author":"Brady Edwin","key":"e_1_3_2_1_9_1","unstructured":"Edwin Brady . 2017. Type-Driven Development with Idris . Manning Publications Co. . isbn:9781617293023 Edwin Brady. 2017. Type-Driven Development with Idris. Manning Publications Co.. isbn:9781617293023"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-28632-5_2"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3354166.3354171"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/321992.321996"},{"volume-title":"Cryptographic Hardware and Embedded Systems, \u00c7etin K","author":"Coron Jean-S\u00e9bastien","key":"e_1_3_2_1_13_1","unstructured":"Jean-S\u00e9bastien Coron . 1999. Resistance Against Differential Power Analysis For Elliptic Curve Cryptosystems . In Cryptographic Hardware and Embedded Systems, \u00c7etin K . Ko\u00e7 and Christof Paar (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg . 292\u2013302. isbn:978-3-540-48059-4 Jean-S\u00e9bastien Coron. 1999. Resistance Against Differential Power Analysis For Elliptic Curve Cryptosystems. In Cryptographic Hardware and Embedded Systems, \u00c7etin K. Ko\u00e7 and Christof Paar (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 292\u2013302. isbn:978-3-540-48059-4"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2006.135"},{"key":"e_1_3_2_1_16_1","volume-title":"Programming in Haskell","author":"Hutton Graham","year":"1871","unstructured":"Graham Hutton . 2007. Programming in Haskell . Cambridge University Press, New York, NY , USA. isbn:052 1871 727, 9780521871723 Graham Hutton. 2007. Programming in Haskell. Cambridge University Press, New York, NY, USA. isbn:0521871727, 9780521871723"},{"key":"e_1_3_2_1_17_1","volume-title":"RPL: A Domain-Specific Language for Designing and Implementing Parallel C++ Applications","author":"Janjic Vladimir","year":"2016","unstructured":"Vladimir Janjic , Christopher Brown , K. Mackenzie , Kevin Hammond , Marco Danelutto , Marco Aldinucci , and Jos\u00e9 Daniel Garc\u00eda . 2016 . RPL: A Domain-Specific Language for Designing and Implementing Parallel C++ Applications . In PDP. IEEE Computer Society , 288\u2013295. Vladimir Janjic, Christopher Brown, K. Mackenzie, Kevin Hammond, Marco Danelutto, Marco Aldinucci, and Jos\u00e9 Daniel Garc\u00eda. 2016. RPL: A Domain-Specific Language for Designing and Implementing Parallel C++ Applications. In PDP. IEEE Computer Society, 288\u2013295."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74735-2_10"},{"volume-title":"Selected Areas in Cryptography, Michael J","author":"Joye Marc","key":"e_1_3_2_1_19_1","unstructured":"Marc Joye . 2009. Highly Regular m-Ary Powering Ladders . In Selected Areas in Cryptography, Michael J . Jacobson, Vincent Rijmen, and Reihaneh Safavi-Naini (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg . 350\u2013363. isbn:978-3-642-05445-7 Marc Joye. 2009. Highly Regular m-Ary Powering Ladders. In Selected Areas in Cryptography, Michael J. Jacobson, Vincent Rijmen, and Reihaneh Safavi-Naini (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 350\u2013363. isbn:978-3-642-05445-7"},{"key":"e_1_3_2_1_20_1","volume-title":"Cryptographic Hardware and Embedded Systems - CHES","author":"Joye Marc","year":"2002","unstructured":"Marc Joye and Sung-Ming Yen . 2003. The Montgomery Powering Ladder . In Cryptographic Hardware and Embedded Systems - CHES 2002 , Burton S. Kaliski, \u00e7etin K. Ko\u00e7, and Christof Paar (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg. 291\u2013302. isbn:978-3-540-36400-9 Marc Joye and Sung-Ming Yen. 2003. The Montgomery Powering Ladder. In Cryptographic Hardware and Embedded Systems - CHES 2002, Burton S. Kaliski, \u00e7etin K. Ko\u00e7, and Christof Paar (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 291\u2013302. isbn:978-3-540-36400-9"},{"volume-title":"Algorithmic Countermeasures Against Fault Attacks and Power Analysis for RSA-CRT","author":"Kiss \u00c1gnes","key":"e_1_3_2_1_21_1","unstructured":"\u00c1gnes Kiss , Juliane Kr\u00e4mer , Pablo Rauzy , and Jean-Pierre Seifert . 2016. Algorithmic Countermeasures Against Fault Attacks and Power Analysis for RSA-CRT . In Constructive Side-Channel Analysis and Secure Design, Fran\u00e7ois-Xavier Standaert and Elisabeth Oswald (Eds.). Springer International Publishing , Cham . 111\u2013129. isbn:978-3-319-43283-0 \u00c1gnes Kiss, Juliane Kr\u00e4mer, Pablo Rauzy, and Jean-Pierre Seifert. 2016. Algorithmic Countermeasures Against Fault Attacks and Power Analysis for RSA-CRT. In Constructive Side-Channel Analysis and Secure Design, Fran\u00e7ois-Xavier Standaert and Elisabeth Oswald (Eds.). Springer International Publishing, Cham. 111\u2013129. isbn:978-3-319-43283-0"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0025-5718-1987-0866109-5"},{"volume-title":"Advances in Cryptology \u2014 CRYPTO","author":"Kocher Paul","key":"e_1_3_2_1_23_1","unstructured":"Paul Kocher , Joshua Jaffe , and Benjamin Jun . 1999. Differential Power Analysis . In Advances in Cryptology \u2014 CRYPTO \u2019 99, Michael Wiener (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg. 388\u2013397. isbn:978-3-540-48405-9 Paul Kocher, Joshua Jaffe, and Benjamin Jun. 1999. Differential Power Analysis. In Advances in Cryptology \u2014 CRYPTO\u2019 99, Michael Wiener (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 388\u2013397. isbn:978-3-540-48405-9"},{"volume-title":"RSA, DSS, and Other Systems. In Advances in Cryptology \u2014 CRYPTO \u201996","author":"Kocher Paul C.","key":"e_1_3_2_1_24_1","unstructured":"Paul C. Kocher . 1996. Timing Attacks on Implementations of Diffie-Hellman , RSA, DSS, and Other Systems. In Advances in Cryptology \u2014 CRYPTO \u201996 , Neal Koblitz (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg . 104\u2013113. isbn:978-3-540-68697-2 Paul C. Kocher. 1996. Timing Attacks on Implementations of Diffie-Hellman, RSA, DSS, and Other Systems. In Advances in Cryptology \u2014 CRYPTO \u201996, Neal Koblitz (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 104\u2013113. isbn:978-3-540-68697-2"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0025-5718-1987-0866113-7"},{"key":"e_1_3_2_1_26_1","unstructured":"S.M. Lane and G. Birkhoff. 1999. Algebra. Chelsea Publishing Company. isbn:9780821816462 lccn:87071728  S.M. Lane and G. Birkhoff. 1999. Algebra. Chelsea Publishing Company. isbn:9780821816462 lccn:87071728"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.3233\/FI-2019-1824"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/ARITH48897.2020.00017"},{"key":"e_1_3_2_1_29_1","volume-title":"ICSOFT (SE)","author":"Maruyama Katsuhisa","year":"2007","unstructured":"Katsuhisa Maruyama . 2007. Secure Refactoring - Improving the Security Level of Existing Code .. In ICSOFT (SE) , Joaquim Filipe, Boris Shishkov, and Markus Helfert (Eds.). INSTICC Press , 222\u2013229. isbn:978-989-8111-06-7 http:\/\/dblp.uni-trier.de\/db\/conf\/icsoft\/icsoft 2007 -2.html##Maruyama07 Katsuhisa Maruyama. 2007. Secure Refactoring - Improving the Security Level of Existing Code.. In ICSOFT (SE), Joaquim Filipe, Boris Shishkov, and Markus Helfert (Eds.). INSTICC Press, 222\u2013229. isbn:978-989-8111-06-7 http:\/\/dblp.uni-trier.de\/db\/conf\/icsoft\/icsoft2007-2.html##Maruyama07"},{"key":"e_1_3_2_1_30_1","unstructured":"A. Menezes P. van Oorschot and S. Vanstone. 1996.. Handbook of Applied Cryptography. CRC Press. isbn:0-8493-8523-7  A. Menezes P. van Oorschot and S. Vanstone. 1996.. Handbook of Applied Cryptography. CRC Press. isbn:0-8493-8523-7"},{"key":"e_1_3_2_1_31_1","volume-title":"Proceedings, Hugh C. Williams (Ed.). Springer Berlin Heidelberg","author":"Miller Victor S.","year":"1986","unstructured":"Victor S. Miller . 1986 . Use of Elliptic Curves in Cryptography. In Advances in Cryptology \u2014 CRYPTO \u201985 Proceedings, Hugh C. Williams (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg. 417\u2013426. isbn:978-3-540-39799-1 Victor S. Miller. 1986. Use of Elliptic Curves in Cryptography. In Advances in Cryptology \u2014 CRYPTO \u201985 Proceedings, Hugh C. Williams (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 417\u2013426. isbn:978-3-540-39799-1"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.infsof.2017.11.010"},{"key":"e_1_3_2_1_33_1","unstructured":"William Opdyke and Ralph Johnson. 1992. Refactoring Object-Oriented Frameworks.  William Opdyke and Ralph Johnson. 1992. Refactoring Object-Oriented Frameworks."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/359340.359342"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-05998-9_13"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-62075-6_4"},{"key":"e_1_3_2_1_37_1","volume-title":"Information Security and Cryptology \u2014 ICISC","author":"Sung-Ming Yen","year":"2001","unstructured":"Yen Sung-Ming , Seungjoo Kim , Seongan Lim , and Sangjae Moon . 2002. A Countermeasure against One Physical Cryptanalysis May Benefit Another Attack . In Information Security and Cryptology \u2014 ICISC 2001 , Kwangjo Kim (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg. 414\u2013427. isbn:978-3-540-45861-6 Yen Sung-Ming, Seungjoo Kim, Seongan Lim, and Sangjae Moon. 2002. A Countermeasure against One Physical Cryptanalysis May Benefit Another Attack. In Information Security and Cryptology \u2014 ICISC 2001, Kwangjo Kim (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 414\u2013427. isbn:978-3-540-45861-6"},{"key":"e_1_3_2_1_38_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_39_1","first-page":"1","article-title":"The Montgomery and Joye Powering Ladders are Dual","volume":"1081","author":"Walter C. D.","year":"2017","unstructured":"C. D. Walter . 2017 . The Montgomery and Joye Powering Ladders are Dual . IACR ePrint Archive , 1081 (2017), 1 \u2013 6 . https:\/\/eprint.iacr.org\/2017\/1081.pdf C. D. Walter. 2017. The Montgomery and Joye Powering Ladders are Dual. IACR ePrint Archive, 1081 (2017), 1\u20136. https:\/\/eprint.iacr.org\/2017\/1081.pdf","journal-title":"IACR ePrint Archive"},{"issue":"2","key":"e_1_3_2_1_40_1","first-page":"171","article-title":"A Survey on Fault Injection Techniques","volume":"1","author":"Ziade H.","year":"2004","unstructured":"H. Ziade , R. Ayoubi , and R. Velazco . 2004 . A Survey on Fault Injection Techniques . International Arab Journal of Information Technology , Vol. 1 , No. 2 , July (2004), 171 \u2013 186 . https:\/\/hal.archives-ouvertes.fr\/hal-00105562 H. Ziade, R. Ayoubi, and R. Velazco. 2004. A Survey on Fault Injection Techniques. International Arab Journal of Information Technology, Vol. 1, No. 2, July (2004), 171\u2013186. https:\/\/hal.archives-ouvertes.fr\/hal-00105562","journal-title":"International Arab Journal of Information Technology"}],"event":{"name":"POPL '22: The 49th Annual ACM SIGPLAN Symposium on Principles of Programming Languages","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"Philadelphia PA USA","acronym":"POPL '22"},"container-title":["Proceedings of the 2022 ACM SIGPLAN International Workshop on Partial Evaluation and Program Manipulation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498886.3502202","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3498886.3502202","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:30:37Z","timestamp":1750188637000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498886.3502202"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,15]]},"references-count":40,"alternative-id":["10.1145\/3498886.3502202","10.1145\/3498886"],"URL":"https:\/\/doi.org\/10.1145\/3498886.3502202","relation":{},"subject":[],"published":{"date-parts":[[2022,1,15]]},"assertion":[{"value":"2022-01-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}