Travelled to:1 × Denmark
1 × Italy
1 × Spain
3 × USA
Collaborated with:C.McBride Darius Mercadier A.Kennedy N.Benton J.B.Jensen J.Chapman P.Morris C.Fournet N.Swamy J.Chen P.Strub B.Livshits T.Bourke Lélio Brun X.Leroy M.Pouzet L.Rieg A.Baumann P.Barham T.L.Harris R.Isaacs S.Peter T.Roscoe A.Schüpbach A.Singhania
Talks about:ornament (2) compil (2) multikernel (1) architectur (1) throughput (1) javascript (1) treatment (1) transport (1) construct (1) multicor (1)
Person: Pierre-Évariste Dagand
DBLP: Dagand:Pierre==Eacute=variste
Contributed to:
2013
2013
2013
20122010
2009
20172019Wrote 8 papers:
- LICS-2013-DagandM #category theory
- A Categorical Treatment of Ornaments (PÉD, CM), pp. 530–539.
- POPL-2013-FournetSCDSL #compilation #javascript
- Fully abstract compilation to JavaScript (CF, NS, JC, PÉD, PYS, BL), pp. 371–384.
- PPDP-2013-KennedyBJD #assembly #coq #metaprogramming #named #question
- Coq: the world’s best macro assembler? (AK, NB, JBJ, PÉD), pp. 13–24.
- ICFP-2012-DagandM
- Transporting functions across ornaments (PÉD, CM), pp. 103–114.
- ICFP-2010-ChapmanDMM
- The gentle art of levitation (JC, PÉD, CM, PM), pp. 3–14.
- SOSP-2009-BaumannBDHIPRSS #architecture #kernel #manycore #scalability
- The multikernel: a new OS architecture for scalable multicore systems (AB, PB, PÉD, TLH, RI, SP, TR, AS, AS), pp. 29–44.
- PLDI-2017-BourkeBDLPR #compilation
- A formally verified compiler for Lustre (TB, LB, PÉD, XL, MP, LR), pp. 586–601.
- PLDI-2019-MercadierD #named
- Usuba: high-throughput and constant-time ciphers, by construction (DM, PÉD), pp. 157–173.