Pierre-Évariste Dagand

According to our database, Pierre-Évariste Dagand authored at least 26 papers between 2009 and 2024.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

2024

Random-Access Lists, from EE to FP.

Titouan Quennet, Pierre-Évariste Dagand

Proceedings of the Programming Languages and Systems - 22nd Asian Symposium, 2024

2021

Reaching for the Star: Tale of a Monad in Coq.

Pierre Nigron, Pierre-Évariste Dagand

Proceedings of the 12th International Conference on Interactive Theorem Proving, 2021

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

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

Intermittent Computing with Peripherals, Formally Verified.

Gautier Berthou, Pierre-Évariste Dagand, Delphine Demange, Rémi Oudin, Tanguy Risset

Proceedings of the 21st ACM SIGPLAN/SIGBED International Conference on Languages, 2020

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

Dependent Pearl: Normalization by realizability.

Pierre-Évariste Dagand, Lionel Rieg, Gabriel Scherer

CoRR, 2019

Usuba: high-throughput and constant-time ciphers, by construction.

Darius Mercadier, Pierre-Évariste Dagand

Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2019

2018

Foundations of dependent interoperability.

Pierre-Évariste Dagand, Nicolas Tabareau, Éric Tanter

J. Funct. Program., 2018

Usuba: Optimizing & Trustworthy Bitslicing Compiler.

Darius Mercadier, Pierre-Évariste Dagand, Lionel Lacassagne, Gilles Muller

Proceedings of the 4th Workshop on Programming Models for SIMD/Vector Processing, 2018

2017

The essence of ornaments.

Pierre-Évariste Dagand

J. Funct. Program., 2017

A formally verified compiler for Lustre.

Timothy Bourke, Lélio Brun, Pierre-Évariste Dagand, Xavier Leroy, Marc Pouzet, Lionel Rieg

Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2017

Type-directed diffing of structured data.

Victor Cacciari Miraldo, Pierre-Évariste Dagand, Wouter Swierstra

Proceedings of the 2nd ACM SIGPLAN International Workshop on Type-Driven Development, 2017

2016

Partial type equivalences for verified dependent interoperability.

Pierre-Évariste Dagand, Nicolas Tabareau, Éric Tanter

Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, 2016

From Sets to Bits in Coq.

Arthur Blot, Pierre-Évariste Dagand, Julia Lawall

Proceedings of the Functional and Logic Programming - 13th International Symposium, 2016

2014

Transporting functions across ornaments.

Pierre-Évariste Dagand, Conor McBride

J. Funct. Program., 2014

Ornaments in practice.

Thomas Williams, Pierre-Évariste Dagand, Didier Rémy

Proceedings of the 10th ACM SIGPLAN workshop on Generic programming, 2014

2013

A cosmology of datatypes : reusability and dependent types.

Pierre-Évariste Dagand

PhD thesis, 2013

Coq: the world's best macro assembler?

Andrew Kennedy, Nick Benton, Jonas Braband Jensen, Pierre-Évariste Dagand

Proceedings of the 15th International Symposium on Principles and Practice of Declarative Programming, 2013

Fully abstract compilation to JavaScript.

Cédric Fournet, Nikhil Swamy, Juan Chen, Pierre-Évariste Dagand, Pierre-Yves Strub, Benjamin Livshits

Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2013

A Categorical Treatment of Ornaments.

Pierre-Évariste Dagand, Conor McBride

Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science, 2013

2012

Elaborating Inductive Definitions

Pierre-Évariste Dagand, Conor McBride

CoRR, 2012

2010

The gentle art of levitation.

James Chapman, Pierre-Évariste Dagand, Conor McBride, Peter Morris

Proceedings of the Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, 2010

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

Opis: reliable distributed systems in OCaml.

Pierre-Évariste Dagand, Dejan Kostic, Viktor Kuncak

Proceedings of TLDI'09: 2009 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, 2009

The multikernel: a new OS architecture for scalable multicore systems.

Andrew Baumann, Paul Barham, Pierre-Évariste Dagand, Tim Harris, Rebecca Isaacs, Simon Peter, Timothy Roscoe, Adrian Schüpbach, Akhilesh Singhania

Proceedings of the 22nd ACM Symposium on Operating Systems Principles 2009, 2009