The multikernel: a new OS architecture for scalable multicore systems. - Andrew Baumann; Paul Barham 001; Pierre-Évariste Dagand; Tim Harris 001; Rebecca Isaacs; Simon Peter 001; Timothy Roscoe; Adrian Schüpbach; Akhilesh Singhania (SOSP, 2009)

Opis: reliable distributed systems in OCaml. - Pierre-Évariste Dagand; Dejan Kostic; Viktor Kuncak (TLDI, 2009)

Filet-o-fish: practical and dependable domain-specific languages for OS development. - Pierre-Évariste Dagand; Andrew Baumann; Timothy Roscoe (ACM SIGOPS Oper. Syst. Rev., 2009)

The gentle art of levitation. - James Chapman 001; Pierre-Évariste Dagand; Conor McBride; Peter Morris (ICFP, 2010)

Elaborating Inductive Definitions - Pierre-Évariste Dagand; Conor McBride (CoRR, 2012)

A Categorical Treatment of Ornaments. - Pierre-Évariste Dagand; Conor McBride (LICS, 2013)

Fully abstract compilation to JavaScript. - Cédric Fournet; Nikhil Swamy; Juan Chen 002; Pierre-Évariste Dagand; Pierre-Yves Strub; Benjamin Livshits (POPL, 2013)

Coq: the world's best macro assembler? - Andrew Kennedy; Nick Benton; Jonas Braband Jensen; Pierre-Évariste Dagand (PPDP, 2013)

A cosmology of datatypes : reusability and dependent types. - Pierre-Évariste Dagand (2013)

Ornaments in practice. - Thomas Williams; Pierre-Évariste Dagand; Didier Rémy (WGP@ICFP, 2014)

Transporting functions across ornaments. - Pierre-Évariste Dagand; Conor McBride (J. Funct. Program., 2014)

From Sets to Bits in Coq. - Arthur Blot; Pierre-Évariste Dagand; Julia Lawall (FLOPS, 2016)

Partial type equivalences for verified dependent interoperability. - Pierre-Évariste Dagand; Nicolas Tabareau; Éric Tanter (ICFP, 2016)

Type-directed diffing of structured data. - Victor Cacciari Miraldo; Pierre-Évariste Dagand; Wouter Swierstra (TyDe@ICFP, 2017)

A formally verified compiler for Lustre. - Timothy Bourke; Lélio Brun; Pierre-Évariste Dagand; Xavier Leroy; Marc Pouzet; Lionel Rieg (PLDI, 2017)

The essence of ornaments. - Pierre-Évariste Dagand (J. Funct. Program., 2017)

Usuba: Optimizing & Trustworthy Bitslicing Compiler. - Darius Mercadier; Pierre-Évariste Dagand; Lionel Lacassagne; Gilles Muller (WPMVP@PPoPP, 2018)

Foundations of dependent interoperability. - Pierre-Évariste Dagand; Nicolas Tabareau; Éric Tanter (J. Funct. Program., 2018)

Usuba: high-throughput and constant-time ciphers, by construction. - Darius Mercadier; Pierre-Évariste Dagand (PLDI, 2019)

Dependent Pearl: Normalization by realizability. - Pierre-Évariste Dagand; Lionel Rieg; Gabriel Scherer (CoRR, 2019)

SKIVA: Flexible and Modular Side-channel and Fault Countermeasures. - Pantea Kiaei; Darius Mercadier; Pierre-Évariste Dagand; Karine Heydemann; Patrick Schaumont (IACR Cryptol. ePrint Arch., 2019)

Intermittent Computing with Peripherals, Formally Verified. - Gautier Berthou 001; Pierre-Évariste Dagand; Delphine Demange; Rémi Oudin; Tanguy Risset (LCTES, 2020)

Tornado: Automatic Generation of Probing-Secure Masked Bitsliced Implementations. - Sonia Belaïd; Pierre-Évariste Dagand; Darius Mercadier; Matthieu Rivain; Raphaël Wintersdorff (IACR Cryptol. ePrint Arch., 2020)

Custom Instruction Support for Modular Defense against Side-channel and Fault Attacks. - Pantea Kiaei; Darius Mercadier; Pierre-Évariste Dagand; Karine Heydemann; Patrick Schaumont (IACR Cryptol. ePrint Arch., 2020)

Reaching for the Star: Tale of a Monad in Coq. - Pierre Nigron; Pierre-Évariste Dagand (ITP, 2021)

Random-Access Lists, from EE to FP. - Titouan Quennet; Pierre-Évariste Dagand (APLAS, 2024)