Publications 2016-2021

• 2021
  • P. Nigron, P.‑E. Dagand : “Reaching for the Star: Tale of a Monad in Coq”, Leibniz International Proceedings in Informatics, vol. 193, Leibniz International Proceedings in Informatics (LIPIcs), Rome, Italy, pp. 29:1-29:19, (Schloss Dagstuhl) (2021)
• 2020
  • P. Kiaei, D. Mercadier, P.‑E. Dagand, K. Heydemann, P. Schaumont : “Custom Instruction Support for Modular Defense against Side-channel and Fault Attacks”, International Workshop on Constructive Side-Channel Analysis and Secure Design, COSADE 2020, Lecture Notes in Computer Science, Lugano, Switzerland (2020)
  • G. Berthou, P.‑E. Dagand, D. Demange, R. Oudin, T. Risset : “Intermittent Computing with Peripherals, Formally Verified”, LCTES '20: 21^st ACM SIGPLAN/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems Proceedings, London / Virtual, United Kingdom, pp. 85-96, (ACM) (2020)
  • S. Belaid, P.‑E. Dagand, D. Mercadier, M. Rivain, R. Wintersdorff : “Tornado: Automatic Generation of Probing-Secure Masked Bitsliced Implementations”, EUROCRYPT, vol. 12107, Lecture Notes in Computer Science, Zagreb / Virtual, Croatia, pp. 311-341, (Springer) (2020)
• 2019
  • D. Mercadier, P.‑E. Dagand : “Usuba: high-throughput and constant-time ciphers, by construction”, PLDI 2019 - 40^th ACM SIGPLAN Conference on Programming Language Design and Implementation, Phoenix, United States, pp. 157-173, (ACM Press) (2019)
• 2018
  • P.‑E. Dagand, N. Tabareau, É. Tanter : “Foundations of Dependent Interoperability”, Journal of Functional Programming, vol. 28, (Cambridge University Press (CUP)) (2018)
  • D. Mercadier, P.‑E. Dagand, L. Lacassagne, G. Muller : “Usuba, Optimizing & Trustworthy Bitslicing Compiler”, WPMVP’18 - Workshop on Programming Models for SIMD/Vector Processing, Vienna, Austria, (ACM Press) (2018)
• 2017
  • T. Bourke, L. Brun, P.‑E. Dagand, X. Leroy, M. Pouzet, L. Rieg : “A Formally Verified Compiler for Lustre”, Proceedings of the 38^th ACM SIGPLAN Conference on Programming Language Design and Implementation, Barcelone, Spain (2017)
  • T. Bourke, P.‑E. Dagand, M. Pouzet, L. Rieg : “Vérification de la génération modulaire du code impératif pour Lustre”, JFLA 2017 - Vingt-huitième Journées Francophones des Langages Applicatifs, Gourette, France (2017)
  • P.‑E. Dagand : “The essence of ornaments”, Journal of Functional Programming, vol. 27, (Cambridge University Press (CUP)) (2017)
  • V. Miraldo, P.‑E. Dagand, W. Swierstra : “Type-directed diffing of structured data”, TyDe 2017 - 2^nd ACM SIGPLAN International Workshop on Type-Driven Development, Oxford, United Kingdom, pp. 2-15, (ACM) (2017)
• 2016
  • P.‑E. Dagand, N. Tabareau, É. Tanter : “Partial Type Equivalences for Verified Dependent Interoperability”, ICFP 2016 - 21^st ACM SIGPLAN International Conference on Functional Programming, Nara, Japan, pp. 298-310 (2016)
  • A. Blot, P.‑E. Dagand, J. Lawall : “From Sets to Bits in Coq”, FLOPS 2016, Kochi, Japan (2016)