Departure date : 03/31/2021
Two past PhD students (2020 - 2022) at Sorbonne University
- 2022
- NIGRON Pierre : Programmes avec effets et leurs preuves dans la théorie des types : application à la compilation certifiée et aux traitements de paquets certifiés.
- 2020
- MERCADIER Darius : Usuba, Optimizing Bitslicing Compiler.
2016-2021 Publications
-
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: 21st 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 - 40th 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 38th 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 - 2nd 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 - 21st 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)