Pierre-Évariste Dagand

33 papers A* 5A 3B 3C 1Misc 1Journal 11Unranked 7
YearRankTypeTitle / Venue / Authors
2024 B conf
Random-Access Lists, from EE to FP.
APLAS
Titouan Quennet, Pierre-Évariste Dagand
2023 — ed.
Proceedings of the 8th ACM SIGPLAN International Workshop on Type-Driven Development, TyDe 2023, Seattle, WA, USA, 4 September 2023
TyDe@ICFP
Youyou Cong, Pierre-Évariste Dagand
2021 B conf
Reaching for the Star: Tale of a Monad in Coq.
ITP
Pierre Nigron, Pierre-Évariste Dagand
2020 — conf
Custom Instruction Support for Modular Defense Against Side-Channel and Fault Attacks.
COSADE
Pantea Kiaei, Darius Mercadier, Pierre-Évariste Dagand, Karine Heydemann, Patrick Schaumont
2020 J jnl
Custom Instruction Support for Modular Defense against Side-channel and Fault Attacks.
IACR Cryptol. ePrint Arch.
Pantea Kiaei, Darius Mercadier, Pierre-Évariste Dagand, Karine Heydemann, Patrick Schaumont
2020 B conf
Intermittent Computing with Peripherals, Formally Verified.
LCTES
Gautier Berthou, Pierre-Évariste Dagand, Delphine Demange, Rémi Oudin, Tanguy Risset
2020 — conf
Tornado: Automatic Generation of Probing-Secure Masked Bitsliced Implementations.
EUROCRYPT (3)
Sonia Belaïd, Pierre-Évariste Dagand, Darius Mercadier, Matthieu Rivain, Raphaël Wintersdorff
2020 J jnl
Tornado: Automatic Generation of Probing-Secure Masked Bitsliced Implementations.
IACR Cryptol. ePrint Arch.
Sonia Belaïd, Pierre-Évariste Dagand, Darius Mercadier, Matthieu Rivain, Raphaël Wintersdorff
2019 J jnl
Dependent Pearl: Normalization by realizability.
CoRR
Pierre-Évariste Dagand, Lionel Rieg, Gabriel Scherer
2019 J jnl
SKIVA: Flexible and Modular Side-channel and Fault Countermeasures.
IACR Cryptol. ePrint Arch.
Pantea Kiaei, Darius Mercadier, Pierre-Évariste Dagand, Karine Heydemann, Patrick Schaumont
2019 A* conf
Usuba: high-throughput and constant-time ciphers, by construction.
PLDI
Darius Mercadier, Pierre-Évariste Dagand
2018 J jnl
Foundations of dependent interoperability.
J. Funct. Program.
Pierre-Évariste Dagand, Nicolas Tabareau, Éric Tanter
2018 — conf
Usuba: Optimizing & Trustworthy Bitslicing Compiler.
WPMVP@PPoPP
Darius Mercadier, Pierre-Évariste Dagand, Lionel Lacassagne, Gilles Muller
2017 A* conf
A formally verified compiler for Lustre.
PLDI
Timothy Bourke, Lélio Brun, Pierre-Évariste Dagand, Xavier Leroy, Marc Pouzet, Lionel Rieg
2017 J jnl
The essence of ornaments.
J. Funct. Program.
Pierre-Évariste Dagand
2017 — conf
Type-directed diffing of structured data.
TyDe@ICFP
Victor Cacciari Miraldo, Pierre-Évariste Dagand, Wouter Swierstra
2016 Misc conf
From Sets to Bits in Coq.
FLOPS
Arthur Blot, Pierre-Évariste Dagand, Julia Lawall
2016 A conf
Partial type equivalences for verified dependent interoperability.
ICFP
Pierre-Évariste Dagand, Nicolas Tabareau, Éric Tanter
2014 — conf
Ornaments in practice.
WGP@ICFP
Thomas Williams, Pierre-Évariste Dagand, Didier Rémy
2014 J jnl
Transporting functions across ornaments.
J. Funct. Program.
Pierre-Évariste Dagand, Conor McBride
2013 A* conf
A Categorical Treatment of Ornaments.
LICS
Pierre-Évariste Dagand, Conor McBride
2013 — —
A cosmology of datatypes : reusability and dependent types.
Pierre-Évariste Dagand
2013 C conf
Coq: the world's best macro assembler?
PPDP
Andrew Kennedy, Nick Benton, Jonas Braband Jensen, Pierre-Évariste Dagand
2013 A* conf
Fully abstract compilation to JavaScript.
POPL
Cédric Fournet, Nikhil Swamy, Juan Chen, Pierre-Évariste Dagand, Pierre-Yves Strub, Benjamin Livshits
2012 J jnl
A Categorical Treatment of Ornaments
CoRR
Pierre-Évariste Dagand, Conor McBride
2012 J jnl
Elaborating Inductive Definitions
CoRR
Pierre-Évariste Dagand, Conor McBride
2012 J jnl
Transporting Functions across Ornaments
CoRR
Pierre-Évariste Dagand, Conor McBride
2012 A conf
Transporting functions across ornaments.
ICFP
Pierre-Évariste Dagand, Conor McBride
2010 A conf
The gentle art of levitation.
ICFP
James Chapman, Pierre-Évariste Dagand, Conor McBride, Peter Morris
2009 — conf
Filet-o-Fish: practical and dependable domain-specific languages for OS development.
PLOS@SOSP
Pierre-Évariste Dagand, Andrew Baumann, Timothy Roscoe
2009 J jnl
Filet-o-fish: practical and dependable domain-specific languages for OS development.
ACM SIGOPS Oper. Syst. Rev.
Pierre-Évariste Dagand, Andrew Baumann, Timothy Roscoe
2009 — conf
Opis: reliable distributed systems in OCaml.
TLDI
Pierre-Évariste Dagand, Dejan Kostic, Viktor Kuncak
2009 A* conf
The multikernel: a new OS architecture for scalable multicore systems.
SOSP
Andrew Baumann, Paul Barham, Pierre-Évariste Dagand, Tim Harris, Rebecca Isaacs, Simon Peter, Timothy Roscoe, Adrian Schüpbach, Akhilesh Singhania