Travelled to:1 × Denmark
1 × Estonia
1 × France
1 × Germany
1 × India
1 × Japan
1 × Portugal
1 × Spain
1 × United Kingdom
10 × USA
3 × Canada
3 × Italy
Collaborated with:V.Vafeiadis C.Hur L.Birkedal G.Neis ∅ A.Rossberg A.Turon N.R.Krishnaswami A.Ahmed J.Kang R.J.0002 Hoang-Hai Dang J.Jourdan J.Kaiser O.Lahav R.Harper D.G.0001 M.Blume D.Swasey B.Ziliani A.Nanevski R.Krebbers J.Tassarotti K.Crary S.Kilpatrick S.L.P.Jones S.Marlow D.Garg G.Gonthier M.M.T.Chakravarty G.Keller Michael Sammler T.Litak A.J.Turon J.Thamsborg Yoonseung Kim C.McLaughlin A.Bizjak R.Jung F.Sieczkowski K.Svendsen R.Lepigre Gaurav Parthasarathy M.Rapoport Amin Timany B.J.0002
Talks about:logic (12) type (8) relat (7) higher (6) order (6) concurr (5) memori (5) separ (5) system (4) reason (4)
Person: Derek Dreyer
DBLP: Dreyer:Derek
Contributed to:
2015
2015
2015
20142014
201320132013201220122011
20112011201020102009200920092008
2007200720072005200420032017
2017201720162017201720182020Wrote 38 papers:
- ICFP-2015-NeisHKMDV #compilation #higher-order #imperative #named
- Pilsner: a compositionally verified compiler for a higher-order imperative language (GN, CKH, JOK, CM, DD, VV), pp. 166–178.
- PLDI-2015-TassarottiDV #logic #memory management #verification
- Verifying read-copy-update in a logic for weak memory (JT, DD, VV), pp. 110–120.
- POPL-2015-JungSSSTBD #concurrent #invariant #monad #named #orthogonal #reasoning
- Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning (RJ, DS, FS, KS, AT, LB, DD), pp. 637–650.
- OOPSLA-2014-TuronVD #memory management #named #navigation #protocol
- GPS: navigating weak memory with ghosts, protocols, and separation (AT, VV, DD), pp. 691–707.
- POPL-2014-KilpatrickDJM #haskell #interface #named
- Backpack: retrofitting Haskell with interfaces (SK, DD, SLPJ, SM), pp. 19–32.
- CSL-2013-KrishnaswamiD #calculus #parametricity #relational
- Internalizing Relational Parametricity in the Extensional Calculus of Constructions (NRK, DD), pp. 432–451.
- ICFP-2013-TuronDB #concurrent #higher-order #hoare #logic #reasoning #refinement
- Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency (AT, DD, LB), pp. 377–390.
- ICFP-2013-ZilianiDKNV #coq #monad #named #programming
- Mtac: a monad for typed tactic programming in Coq (BZ, DD, NRK, AN, VV), pp. 87–100.
- POPL-2013-HurNDV #induction #power of #proving
- The power of parameterization in coinductive proof (CKH, GN, DD, VV), pp. 193–206.
- POPL-2013-TuronTABD #concurrent #fine-grained #logic
- Logical relations for fine-grained concurrency (AJT, JT, AA, LB, DD), pp. 343–356.
- ICFP-2012-KrishnaswamiTDG
- Superficially substructural types (NRK, AT, DD, DG), pp. 41–54.
- POPL-2012-HurDNV #bisimulation #logic
- The marriage of bisimulations and Kripke logical relations (CKH, DD, GN, VV), pp. 59–72.
- ICFP-2011-GonthierZND #ad hoc #automation #how #proving
- How to make ad hoc proof automation less ad hoc (GG, BZ, AN, DD), pp. 163–175.
- LICS-2011-HurDV #garbage collection #logic
- Separation Logic in the Presence of Garbage Collection (CKH, DD, VV), pp. 247–256.
- POPL-2011-HurD #assembly #logic #ml
- A kripke logical relation between ML and assembly (CKH, DD), pp. 133–146.
- ICFP-2010-DreyerNB #higher-order #reasoning #relational
- The impact of higher-order state and control effects on local relational reasoning (DD, GN, LB), pp. 143–156.
- POPL-2010-DreyerNRB #data type #higher-order #logic #relational
- A relational modal logic for higher-order stateful ADTs (DD, GN, AR, LB), pp. 185–198.
- ICFP-2009-NeisDR #parametricity
- Non-parametric parametricity (GN, DD, AR), pp. 135–148.
- LICS-2009-DreyerAB #logic
- Logical Step-Indexed Logical Relations (DD, AA, LB), pp. 71–80.
- POPL-2009-AhmedDR #independence #representation
- State-dependent representation independence (AA, DD, AR), pp. 340–353.
- ICFP-2008-DreyerR #mixin #ml
- Mixin’ up the ML module system (DD, AR), pp. 307–320.
- ESOP-2007-DreyerB #composition #source code
- Principal Type Schemes for Modular Programs (DD, MB), pp. 441–457.
- ICFP-2007-Dreyer #recursion #type system
- A type system for recursive modules (DD), pp. 289–302.
- POPL-2007-DreyerHCK #composition
- Modular type classes (DD, RH, MMTC, GK), pp. 63–70.
- ICFP-2005-Dreyer #recursion
- Recursive type generativity (DD), pp. 41–53.
- POPL-2004-Dreyer #recursion #type system
- A type system for well-founded recursion (DD), pp. 293–305.
- POPL-2003-DreyerCH #higher-order #type system
- A type system for higher-order modules (DD, KC, RH), pp. 236–249.
- ESOP-2017-Krebbers0BJDB #concurrent #higher-order #logic
- The Essence of Higher-Order Concurrent Separation Logic (RK, RJ0, AB, JHJ, DD, LB), pp. 696–723.
- ECOOP-2017-KaiserDDLV #consistency #logic #memory management #reasoning
- Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris (JOK, HHD, DD, OL, VV), p. 29.
- OOPSLA-2017-Swasey0D #composition #robust #verification
- Robust and compositional verification of object capability patterns (DS, DG0, DD), p. 26.
- POPL-2016-KangKHDV #compilation #lightweight #verification
- Lightweight verification of separate compilation (JK, YK, CKH, DD, VV), pp. 178–190.
- PLDI-2017-LahavVKHD #consistency
- Repairing sequential consistency in C/C++11 (OL, VV, JK, CKH, DD), pp. 618–632.
- POPL-2017-KangHLVD #concurrent #semantics
- A promising semantics for relaxed-memory concurrency (JK, CKH, OL, VV, DD), pp. 175–189.
- POPL-2018-0002JKD #named #programming language #rust
- RustBelt: securing the foundations of the rust programming language (RJ0, JHJ, RK, DD), p. 34.
- POPL-2020-DangJKD #memory management
- RustBelt meets relaxed memory (HHD, JHJ, JOK, DD), p. 29.
- POPL-2020-JungDKD #alias #rust
- Stacked borrows: an aliasing model for Rust (RJ0, HHD, JK, DD), p. 32.
- POPL-2020-JungLPRTDJ #logic
- The future is ours: prophecy variables in separation logic (RJ0, RL, GP, MR, AT, DD, BJ0), p. 32.
- POPL-2020-SammlerGDL #low level
- The high-level benefits of low-level sandboxing (MS, DG0, DD, TL), p. 32.