Recherche - Archive ouverte HAL Accéder directement au contenu

Filtrer vos résultats

19 résultats
Page :
triés par
Image document

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

 Darius Mercadier , Pierre-Evariste Dagand
PLDI 2019 - 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, Jun 2019, Phoenix, United States. pp.157-173, ⟨10.1145/3314221.3314636⟩
Communication dans un congrès hal-02176603v1
Image document

Tornado: Automatic Generation of Probing-Secure Masked Bitsliced Implementations

 Sonia Belaïd , Pierre-Evariste Dagand , Darius Mercadier , Matthieu Rivain , Raphaël Wintersdorff
Eurocrypt 2020 - 39th Annual International Conference on the Theory and Applications of Cryptographic Techniques, May 2020, Zagreb / Virtual, Croatia. pp.311-341, ⟨10.1007/978-3-030-45727-3_11⟩
Communication dans un congrès hal-02953167v1

Coq: the world's best macro assembler?

 Nick Benton , Andrew Kennedy , Jonas Jensen , Pierre-Évariste Dagand
PPDP 2013: ACM Symposium on Principles and Practice of Declarative Programming, Sep 2013, Madrid, Spain. ⟨10.1145/2505879.2505897⟩
Communication dans un congrès hal-01081548v1
Image document

Reaching for the Star: Tale of a Monad in Coq

 Pierre Nigron , Pierre-Évariste Dagand
12th International Conference on Interactive Theorem Proving (ITP 2021), Jun 2021, Rome, Italy. pp.29:1--29:19, ⟨10.4230/LIPIcs.ITP.2021.29⟩
Communication dans un congrès hal-03266768v1
Image document

Foundations of Dependent Interoperability

 Pierre-Evariste Dagand , Nicolas Tabareau , Éric Tanter
Journal of Functional Programming, 2018, 28, ⟨10.1017/S0956796818000011⟩
Article dans une revue hal-01629909v2
Image document

A Formally Verified Compiler for Lustre

 Timothy Bourke , Lélio Brun , Pierre-Evariste Dagand , Xavier Leroy , Marc Pouzet , et al.
PLDI 2017 - 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, ACM, Jun 2017, Barcelone, Spain
Communication dans un congrès hal-01512286v1
Image document

Intermittent Computing with Peripherals, Formally Verified

 Gautier Berthou , Pierre-Evariste Dagand , Delphine Demange , Rémi Oudin , Tanguy Risset
LCTES '20 - 21st ACM SIGPLAN/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems, Jun 2020, London / Virtual, United Kingdom. pp.85-96, ⟨10.1145/3372799.3394365⟩
Communication dans un congrès hal-02556878v1
Image document

Rough Pearl: Manufacturing Cons-Cells

 Pierre-Evariste Dagand , Pierre Letouzey , Ellenor Fatemeh Taghayor
35es Journées Francophones des Langages Applicatifs (JFLA 2024), Jan 2024, Saint-Jacut-de-la-Mer, France
Communication dans un congrès hal-04406422v1

The essence of ornaments

 Pierre-Evariste Dagand
Journal of Functional Programming, 2017, 27, ⟨10.1017/S0956796816000356⟩
Article dans une revue hal-01461209v1
Image document

Normalization by realizability also evaluates

 Pierre-Évariste Dagand , Gabriel Scherer
Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), Jan 2015, Le Val d'Ajol, France
Communication dans un congrès hal-01099138v1
Image document

Elaborating inductive definitions

 Pierre-Evariste Dagand , Conor Mcbride
JFLA - Journées francophones des langages applicatifs, Damien Pous and Christine Tasson, Feb 2013, Aussois, France
Communication dans un congrès hal-00778975v1
Image document

Custom Instruction Support for Modular Defense against Side-channel and Fault Attacks

 Pantea Kiaei , Darius Mercadier , Pierre-Evariste Dagand , Karine Heydemann , Patrick Schaumont
International Workshop on Constructive Side-Channel Analysis and Secure Design, COSADE 2020, Oct 2020, Lugano, Switzerland
Communication dans un congrès hal-03058888v1
Image document

Fully Abstract Compilation to JavaScript

 Cédric Fournet , Nikhil Swamy , Juan Chen , Pierre-Evariste Dagand , Pierre-Yves Strub , et al.
40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - POPL'13 (2013), Jan 2013, Roma, Italy
Communication dans un congrès hal-00780803v1
Image document

A Formal Model of Interrupt-based Checkpointing with Peripherals

 Pierre-Evariste Dagand , Gautier Berthou , Delphine Demange , Tanguy Risset
[Research Report] IRIF; IRISA; INSA RENNES. 2022, pp.1-36
Rapport hal-03557760v1
Image document

Partial Type Equivalences for Verified Dependent Interoperability

 Pierre-Evariste Dagand , Nicolas Tabareau , Éric Tanter
ICFP 2016 - 21st ACM SIGPLAN International Conference on Functional Programming, Sep 2016, Nara, Japan. pp.298-310, ⟨10.1145/2951913.2951933⟩
Communication dans un congrès hal-01328012v1
Image document

Usuba, Optimizing & Trustworthy Bitslicing Compiler

 Darius Mercadier , Pierre-Évariste Dagand , Lionel Lacassagne , Gilles Muller
WPMVP’18 - Workshop on Programming Models for SIMD/Vector Processing, Feb 2018, Vienna, Austria. ⟨10.1145/3178433.3178437⟩
Communication dans un congrès hal-01657259v2

Ornaments in practice

 Thomas Williams , Pierre-Évariste Dagand , Didier Rémy
WGP 2014: ACM workshop on Generic programming, Aug 2014, Gothenburg, Sweden. ⟨10.1145/2633628.2633631⟩
Communication dans un congrès hal-01081547v1

Type-directed diffing of structured data

 Victor Cacciari Miraldo , Pierre-Evariste Dagand , Wouter Swierstra
TyDe 2017 - 2nd ACM SIGPLAN International Workshop on Type-Driven Development, Sep 2017, Oxford, United Kingdom. pp.2-15, ⟨10.1145/3122975.3122976⟩
Communication dans un congrès hal-01673541v1
Image document

Vérification de la génération modulaire du code impératif pour Lustre

 Timothy Bourke , Pierre-Evariste Dagand , Marc Pouzet , Lionel Rieg
JFLA 2017 - Vingt-huitième Journées Francophones des Langages Applicatifs, Jan 2017, Gourette, France
Communication dans un congrès hal-01403830v1
Page :