Pierre-Évariste Dagand

According to our database1, Pierre-Évariste Dagand authored at least 25 papers between 2009 and 2021.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

On csauthors.net:

Bibliography

2021
Reaching for the Star: Tale of a Monad in Coq.
Proceedings of the 12th International Conference on Interactive Theorem Proving, 2021

2020
Custom Instruction Support for Modular Defense against Side-channel and Fault Attacks.
IACR Cryptol. ePrint Arch., 2020

Tornado: Automatic Generation of Probing-Secure Masked Bitsliced Implementations.
IACR Cryptol. ePrint Arch., 2020

Intermittent Computing with Peripherals, Formally Verified.
Proceedings of the 21st ACM SIGPLAN/SIGBED International Conference on Languages, 2020

2019
SKIVA: Flexible and Modular Side-channel and Fault Countermeasures.
IACR Cryptol. ePrint Arch., 2019

Dependent Pearl: Normalization by realizability.
CoRR, 2019

Usuba: high-throughput and constant-time ciphers, by construction.
Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2019

2018
Foundations of dependent interoperability.
J. Funct. Program., 2018

Usuba: Optimizing & Trustworthy Bitslicing Compiler.
Proceedings of the 4th Workshop on Programming Models for SIMD/Vector Processing, 2018

2017
The essence of ornaments.
J. Funct. Program., 2017

A formally verified compiler for Lustre.
Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2017

Type-directed diffing of structured data.
Proceedings of the 2nd ACM SIGPLAN International Workshop on Type-Driven Development, 2017

2016
Partial type equivalences for verified dependent interoperability.
Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, 2016

From Sets to Bits in Coq.
Proceedings of the Functional and Logic Programming - 13th International Symposium, 2016

2014
Transporting functions across ornaments.
J. Funct. Program., 2014

Ornaments in practice.
Proceedings of the 10th ACM SIGPLAN workshop on Generic programming, 2014

2013
A cosmology of datatypes : reusability and dependent types.
PhD thesis, 2013

Coq: the world's best macro assembler?
Proceedings of the 15th International Symposium on Principles and Practice of Declarative Programming, 2013

Fully abstract compilation to JavaScript.
Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2013

A Categorical Treatment of Ornaments.
Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science, 2013

2012
Elaborating Inductive Definitions
CoRR, 2012

2010
The gentle art of levitation.
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.
ACM SIGOPS Oper. Syst. Rev., 2009

Opis: reliable distributed systems in OCaml.
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.
Proceedings of the 22nd ACM Symposium on Operating Systems Principles 2009, 2009


  Loading...