Derek Dreyer → Research
Curriculum Vitae
Research Statement
Professional Activities
Awards and Grants
Research Collaborators and Advisees
Publications
About Me
I am
a
scientific director of
the Max
Planck Institute for Software Systems (MPI-SWS) in Kaiserslautern and
Saarbrücken, Germany.
I work at the Saarbrücken branch of the institute, where I lead the “Foundations
of Programming” Group.
I have been faculty here since
January 2008, received tenure in October 2013, and became a scientific director in May 2022.
In September 2017, I received the ACM SIGPLAN Robin Milner Young Researcher Award.
I was also appointed as an Honorarprofessor of Computer Science at Saarland University,
which means that you can now address me illustriously
as "Herr Professor Derektor Dreyer".
Or if you prefer to follow the lead of my daughter Alma, you can call me "Yb" (pronounced "eeb"),
which is short for "ybab" ("baby" spelled backwards -- don't ask).
Originally, the name of my research group was “Type Systems and
Functional Programming”, but at some point I realized
I was spending most of my time thinking about how to
verify untyped imperative programs — how embarrassing!!
Perhaps a more useful description for my research is
that I am working toward a
“realistic” theory of modularity.
That is, I am trying to figure out how we can build
and reason modularly about programs that use “interesting”
features,
like fine-grained weak-memory concurrency, or higher-order state, or recursive
linking, or dependent types, or self-modifying assembly code (!),
which make these programs so interesting that traditional
semantic and verification techniques cannot account for them.
Toward that end, I supervise a number of terrific students and postdocs working on all sorts of fascinating problems,
and I collaborate with several other researchers in the area of PL/Verification at MPI-SWS and around the world.
I have also been awarded a 2015 ERC Consolidator Grant for the
5-year project “RustBelt”.
In this project, we aim to
build the first formal foundations for safe systems programming in
Mozilla's new language, Rust.
We are actively hiring exceptional postdocs
and PhD students to work on RustBelt -- see here for information on
how to apply.
From 2012 to 2015, I served on the ACM SIGPLAN Executive Committee,
where I chaired the committees for most-influential-paper awards.
I am still actively involved in a variety of SIGPLAN activities, including
steering the Programming Languages Mentoring Workshop (PLMW) series,
which has
helped expose many new students to PL research.
Many people seemed to enjoy my talk at PLMW 2014 on parametricity
and my talks at many subsequent PLMWs on writing and speaking skills.
All of my publications are accessible below, or you can check out my publication page on DBLP or my Google Scholar profile.
I also try to keep my CV up to date.
-
Program chair, 2024 ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2024)
-
Member of the advisory board, Proceedings of the ACM on Programming Languages (PACMPL), July 2023–present
-
Managing director, MPI-SWS, July 2022–present
-
Co-editor-in-chief, Journal of Functional Programming (JFP), February 2022–present
-
General chair, 2019 ACM SIGPLAN International Conference on Functional Programming (ICFP 2019)
- Associate editor, ACM Transactions on Programming Languages and Systems (TOPLAS), July 2017–present
- Editor, Journal of Functional Programming (JFP), July 2019–January 2022
- Member of the editorial board, Journal of Functional Programming (JFP), Feb 2014–June 2019
-
Member-at-large (elected) and awards chair, ACM SIGPLAN Executive Committee, July 2012–June 2015
- Member, IFIP Working Group 2.8 – Functional Programming, Aug 2014–present
- Workshop founder, ACM SIGPLAN Workshop on Higher-Order Programming with Effects (HOPE)
- Lead organizer, Dagstuhl Seminar on Compositional Verification Methods for Next-Generation Concurrency, May 2015
- Lead organizer, The Cornell, Maryland, Max Planck Pre-doctoral Research School 2018 (CMMRS 2018)
- Co-editor, Journal of Functional Programming (JFP): Special issue devoted to ICFP 2014
- Co-editor, Journal of Functional Programming (JFP): Special issue for Robert Harper Festschrift
- Workshop (co-)chair/organizer:
- Program committee (PC) member:
- OOPSLA 2023 (associate chair), CAV 2022, ECOOP 2022, ECOOP 2019, OOPSLA 2018, POPL 2017,
FSCD 2016,
ESOP 2015,
MFPS 2015,
ICFP 2014,
ESOP 2013, CPP 2013, ML 2013,
CC 2012,
POPL 2011,
MLPA 2010,
FOOL 2010,
MFPS 2009,
MLPA 2009,
ICFP 2008,
FOOL/WOOD 2007, Haskell 2007,
ML 2006
- External review committee (ERC) member:
- Steering committee member:
- Invited speaker:
- Seminar Series on Mechanized Semantics, Collège de France (February 2020), OWLS Seminar (December 2020)
- POPL 2018, ESOP 2018, Distinguished Colloquium @ University of Maryland (Sep. 2018)
- CMMRS 2017,
FTfJP 2017,
MFPS 2017,
Computer Science Colloquium @ Cornell University (Nov. 2017)
- ACM SIGPLAN Programming Languages Mentoring Workshop:
- How to Write Papers and Give Talks That People Can Follow, delivered in various versions at
PLMW@ICFP 2022,
PLMW@ICFP 2021,
PLMW@PLDI 2021,
PLMW@ICFP 2020,
PLMW@POPL 2020,
PLMW@SPLASH 2019,
PLMW@ICFP 2019,
PLMW@POPL 2018,
PLMW@ICFP 2017,
PLMW@POPL 2017,
PLMW@ICFP 2016
PLMW@POPL 2016
- Progress and Preservation Considered Boring! A Paean to Parametricity, delivered at PLMW@POPL 2014
- Distinguished Lecture Series @ University of Chicago (May 2016)
- 3rd South of England Regional Programming Languages Seminar (S-REPLS 3, April 2016)
- Workshop on Certification of High-Level and Low-Level Programs,
Institut Henri Poincaré thematic trimester on Semantics of Proofs and Certified Mathematics (July 2014)
- 2014 Oregon Programming Languages Summer School (OPLSS 2014)
- Parametricity Workshop 2012
- LFMTP 2011
- MFPS 2008
-
Selection committee member:
- Workshops co-chair, ICFP 2010 and ICFP 2011
- Staff representative (Mitarbeitervertreter) of MPI-SWS in the CPT Section of the Max Planck Society, 2010–2016
- Moderator, TYPES and TYPES/announce mailing lists, April 2009–April 2014
- Invited participant, IFIP WG2.8 Meeting (July 2007, February 2012)
- Senior member, ACM SIGPLAN
Collaborators at MPI-SWS
Current PhD Students:
Current Postdocs:
Former PhD Students:
-
Hoang-Hai Dang (Apr. 2016–Feb. 2022, now at BlueRock Security)
-
Ralf Jung (Apr. 2014–Aug. 2020, now faculty at ETH Zürich)
-
Jan-Oliver Kaiser (Apr. 2014–May 2020, now at BlueRock Security)
-
Scott Kilpatrick (Aug. 2010–Apr. 2016, now at Two Sigma)
-
Georg Neis (Nov. 2008–Aug. 2015, now at Google)
-
Michael Sammler (May 2019–Dec. 2023, now postdoc at ETH Zürich, to be faculty at IST Austria), co-advised by Deepak Garg
-
David Swasey (Sep. 2012–May 2020, now at BlueRock Security), co-advised by Deepak Garg
-
Joshua Yanovski (July 2017–Oct. 2020)
-
Fengmin (Paul) Zhu (Nov. 2020–Aug. 2021, now PhD student at CISPA)
-
Beta Ziliani (Jan. 2010–Mar. 2015, now principal engineer of the Crystal programming language)
Former Postdocs:
-
Emanuele D'Osualdo (Sep. 2020–Mar. 2024, now faculty at University of Konstanz)
-
Chung-Kil (Gil) Hur (Oct. 2010–Sep. 2012, now faculty at Seoul National University)
-
Jacques-Henri Jourdan (Apr. 2016–Sep. 2017, now at CNRS)
-
Neel Krishnaswami (Sep. 2011–Sep. 2013, now faculty at University of Cambridge)
-
Ori Lahav (Apr. 2016–Sep. 2017, now faculty at Tel Aviv University), co-advised by Viktor Vafeiadis
-
Rodolphe Lepigre (Jan. 2019–Jan. 2022, now at BlueRock Security)
-
Pierre-Marie Pédrot (Oct. 2017–Sep. 2018, now at Inria)
-
Azalea Raad (July 2017–Sep. 2020, now faculty at Imperial College London), co-advised by Viktor Vafeiadis
-
Andreas Rossberg (Aug. 2007–Jan. 2010, was later a lead co-designer of Webassembly)
-
Youngju Song (Nov. 2021–May 2024, now at Amazon)
-
Aaron Turon (Jan. 2013–Apr. 2014, now at Fastly)
Former Interns:
-
Yixuan Chen (Summer 2021, now PhD student at Yale University)
-
Shabnam Ghasemirad (Summer 2019, now PhD student at ETH Zürich)
-
Jeehoon Kang (Fall 2015, now faculty at KAIST)
-
Lisa Kohl (Summer 2013, now researcher at CWI Amsterdam)
-
Yusuke Matsushita (Sep. 2020–June 2021, now postdoc at Kyoto University)
-
Gaurav Parthasarathy (Summer 2018, now PhD student at ETH Zürich)
-
George Pîrlea (Summer 2019, now PhD student at National University of Singapore)
-
Marianna Rapoport (Summer 2018, now at Amazon Web Services)
-
Milijana Surbatovich (Spring 2022, now faculty at University of Maryland)
-
Joseph Tassarotti (Summer 2014, now faculty at NYU)
-
Neven Villani (2022-2023, now student at ENS Paris-Saclay, ongoing collaboration)
-
Irene Yoon (Summer 2021, now postdoc at INRIA Paris, ongoing collaboration)
-
Zhen Zhang (Summer 2016, now software engineer at Google)
Publications
2025:
-
Data Race Freedom à la Mode.
Aïna Linn Georges, Benjamin Peters, Laila Elbeheiry, Leo White, Stephen Dolan, Richard A. Eisenberg, Chris Casinghino, François Pottier, Derek Dreyer.
In 2025 ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2025).
Final Version: (paper in PDF,
artifact)
Official Citation: PACMPL 9, POPL, Article 23, January 2025.
2024:
-
A Logical Approach to Type Soundness.
Amin Timany, Robbert Krebbers, Derek Dreyer, Lars Birkedal.
In Journal of the ACM (JACM), Volume 71, Issue 6, Article No. 40, November 2024.
Final Version: (paper in PDF)
-
Quiver: Guided Abductive Inference of Separation Logic Specifications in Coq.
Simon Spies, Lennard Gäher, Michael Sammler, Derek Dreyer.
In 2024 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2024).
Final Version: (paper in PDF, paper website)
Official Citation: PACMPL 8, PLDI, Article 183, June 2024.
Recipient of PLDI 2024 Distinguished Artifact Award.
-
RefinedRust: A Type System for High-Assurance Verification of Rust Programs.
Lennard Gäher, Michael Sammler, Ralf Jung, Robbert Krebbers, Derek Dreyer.
In 2024 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2024).
Final Version: (paper in PDF, paper website)
Official Citation: PACMPL 8, PLDI, Article 192, June 2024.
2023:
-
Melocoton: A Program Logic for Verified Interoperability Between OCaml and C.
Armaël Guéneau, Johannes Hostert, Simon Spies, Michael Sammler, Lars Birkedal, Derek Dreyer.
In 2023 ACM SIGPLAN International Conference on Object-Oriented Programming,
Systems, Languages, and Applications (OOPSLA 2023).
Final Version: (paper in PDF, paper website and Coq development)
Official Citation: PACMPL 7, OOPSLA2, Article 247, October 2023.
-
Stuttering for Free.
Minki Cho, Youngju Song, Dongjae Lee, Lennard Gäher, Derek Dreyer.
In 2023 ACM SIGPLAN International Conference on Object-Oriented Programming,
Systems, Languages, and Applications (OOPSLA 2023).
Final Version: (paper in PDF, Coq development)
Official Citation: PACMPL 7, OOPSLA2, Article 281, October 2023.
-
Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning.
Noam Zilberstein, Derek Dreyer, Alexandra Silva.
In 2023 ACM SIGPLAN International Conference on Object-Oriented Programming,
Systems, Languages, and Applications (OOPSLA 2023).
Final Version: (paper + appendix in PDF, paper website)
Official Citation: PACMPL 7, OOPSLA1, Article 93, April 2023.
-
DimSum: A Decentralized Approach to Multi-language Semantics and Verification.
Michael Sammler, Simon Spies, Youngju Song, Emanuele D'Osualdo, Robbert Krebbers, Deepak Garg, Derek Dreyer.
In 2023 ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2023).
Final Version: (paper in PDF,
talk slides,
paper website,
artifact)
Official Citation: PACMPL 7, POPL, Article 27, January 2023.
Recipient of POPL 2023 Distinguished Paper Award.
-
Conditional Contextual Refinement.
Youngju Song, Minki Cho, Dongjae Lee, Chung-Kil Hur, Michael Sammler, Derek Dreyer.
In 2023 ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2023).
Final Version: (paper in PDF,
paper website,
artifact)
Official Citation: PACMPL 7, POPL, Article 39, January 2023.
2022:
-
Proving Hypersafety Compositionally.
Emanuele D'Osualdo, Azadeh Farzan, Derek Dreyer.
In 2022 ACM SIGPLAN International Conference on Object-Oriented Programming,
Systems, Languages, and Applications (OOPSLA 2022).
Final Version: (paper in PDF, technical report)
Official Citation: PACMPL 6, OOPSLA2, Article 135, October 2022.
-
BFF: Foundational and Automated Verification of Bitfield-Manipulating Programs.
Fengmin Zhu, Michael Sammler, Rodolphe Lepigre, Derek Dreyer, Deepak Garg.
In 2022 ACM SIGPLAN International Conference on Object-Oriented Programming,
Systems, Languages, and Applications (OOPSLA 2022).
Final Version: (paper in PDF, artifact, paper website)
Official Citation: PACMPL 6, OOPSLA2, Article 182, October 2022.
-
Finding Real Bugs in Big Programs with Incorrectness Logic.
Quang Loc Le, Azalea Raad, Jules Villard, Josh Berdine, Derek Dreyer, Peter W. O'Hearn.
In 2022 ACM SIGPLAN International Conference on Object-Oriented Programming,
Systems, Languages, and Applications (OOPSLA 2022).
Final Version: (paper in PDF, artifact, appendix)
Official Citation: PACMPL 6, OOPSLA1, Article 81, April 2022.
Recipient of OOPSLA 2022 Distinguished Paper Award.
-
Later Credits: Resourceful Reasoning for the Later Modality.
Simon Spies, Lennard Gäher, Joseph Tassarotti, Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer.
In 2022 ACM SIGPLAN International Conference on Functional Programming (ICFP 2022).
Final Version: (paper in PDF, paper website)
Official Citation: PACMPL 6, ICFP, Article 100, August 2022.
-
Compass: Strong and Compositional Library Specifications in Relaxed Memory Separation Logic.
Hoang-Hai Dang, Jaehwang Jung, Jaemin Choi, Duc-Than Nguyen,
William Mansky, Jeehoon Kang, Derek Dreyer.
In 2022 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2022).
Final Version: (paper in PDF, paper website, Coq development)
-
RustHornBelt: A Semantic Foundation for Functional Verification of Rust Programs with Unsafe Code.
Yusuke Matsushita, Xavier Denis, Jacques-Henri Jourdan, Derek Dreyer.
In 2022 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2022).
Final Version: (paper in PDF, artifact, Coq development, Creusot development, errata)
Recipient of PLDI 2022 Distinguished Paper Award.
-
Islaris: Verification of Machine Code Against Authoritative ISA Semantics.
Michael Sammler, Angus Hammond, Rodolphe Lepigre, Brian Campbell,
Jean Pichon-Pharabod, Derek Dreyer, Deepak Garg, Peter Sewell.
In 2022 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2022).
Final Version: (paper in PDF, Coq development)
-
Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations.
Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung,
Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, Derek Dreyer.
In 2022 ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2022).
Final Version: (paper in PDF, Coq development, artifact and appendix)
Official Citation: PACMPL 6, POPL, Article 28, January 2022.
Recipient of POPL 2022 Distinguished Paper Award.
-
VIP: Verifying Real-World C Idioms with Integer-Pointer Casts.
Rodolphe Lepigre, Michael Sammler, Kayvan Memarian, Robbert Krebbers, Derek Dreyer, Peter Sewell.
In 2022 ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2022).
Final Version: (paper in PDF, Coq development, artifact and appendix)
Official Citation: PACMPL 6, POPL, Article 20, January 2022.
-
Concurrent Incorrectness Separation Logic.
Azalea Raad, Josh Berdine, Derek Dreyer, Peter W. O'Hearn.
In 2022 ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2022).
Final Version: (paper in PDF, technical appendix)
Official Citation: PACMPL 6, POPL, Article 34, January 2022.
-
Editorial: On Being a PhD Student of Robert Harper.
Derek Dreyer, Benjamin C. Pierce.
In Journal of Functional Programming (JFP), Volume 32, e3, January 2022.
Robert Harper Festschrift Collection.
Final Version: (editorial in PDF)
2021:
-
GhostCell: Separating Permissions from Data in Rust.
Joshua Yanovski, Hoang-Hai Dang, Ralf Jung, Derek Dreyer.
In 2021 ACM SIGPLAN International Conference on Functional Programming (ICFP 2021).
Final Version: (paper in PDF, website with Coq development)
Official Citation: PACMPL 5, ICFP, Article 92, August 2021.
-
RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Types.
Michael Sammler, Rodolphe Lepigre, Robbert Krebbers, Kayvan Memarian, Derek Dreyer, Deepak Garg.
In 2021 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2021).
Final Version: (paper in PDF, paper website, Coq development)
Recipient of PLDI 2021 Distinguished Paper Award.
Recipient of PLDI 2021 Distinguished Artifact Award.
-
Transfinite Iris: Resolving an Existential Dilemma of Step-Indexed Separation Logic.
Simon Spies, Lennard Gäher, Daniel Gratzer, Joseph Tassarotti, Robbert Krebbers, Derek Dreyer, Lars Birkedal.
In 2021 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2021).
Final Version: (paper in PDF, paper website, Coq development)
-
Safe Systems Programming in Rust.
Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, Derek Dreyer.
Invited contributed article, Communications of the ACM (CACM), 64(4): 144–152, April 2021.
Journal Version: (paper in PDF, paper in HTML, accompanying video)
This is a high-level overview of Rust and RustBelt, intended for a general CS audience.
-
Transfinite Step-Indexing for Termination.
Simon Spies, Neel Krishnaswami, Derek Dreyer.
In 2021 ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2021).
Final Version: (paper in PDF, technical appendix)
Official Citation: PACMPL 5, POPL, Article 13, January 2021.
2020:
-
Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic.
Azalea Raad, Josh Berdine, Hoang-Hai Dang, Derek Dreyer, Peter O'Hearn, Jules Villard.
In 2020 International Conference on Computer-Aided Verification (CAV 2020).
Conference Version: (paper in PDF, paper website)
-
RustBelt Meets Relaxed Memory.
Hoang-Hai Dang, Jacques-Henri Jourdan, Jan-Oliver Kaiser, Derek Dreyer.
In 2020 ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2020).
Final Version: (paper in PDF, website with appendix and Coq development)
Official Citation: PACMPL 4, POPL, Article 34, January 2020.
-
Stacked Borrows: An Aliasing Model for Rust.
Ralf Jung, Hoang-Hai Dang, Jeehoon Kang, Derek Dreyer.
In 2020 ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2020).
Final Version: (paper in PDF, website with appendix and Coq development)
Official Citation: PACMPL 4, POPL, Article 41, January 2020.
-
The Future is Ours: Prophecy Variables in Separation Logic.
Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy,
Marianna Rapoport, Amin Timany, Derek Dreyer, Bart Jacobs.
In 2020 ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2020).
Final Version: (paper in PDF, website with Coq development)
Official Citation: PACMPL 4, POPL, Article 45, January 2020.
-
The High-Level Benefits of Low-Level Sandboxing.
Michael Sammler, Deepak Garg, Derek Dreyer, Tadeusz Litak.
In 2020 ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2020).
Final Version: (paper in PDF, Coq development)
Official Citation: PACMPL 4, POPL, Article 32, January 2020.
2018:
-
Iris from the Ground Up: A Modular Foundation for Higher-Order Concurrent Separation Logic.
Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Aleš Bizjak, Lars Birkedal, Derek Dreyer.
In Journal of Functional Programming (JFP), Volume 28, e20, November 2018.
Special issue devoted to selected papers from ICFP 2016.
Journal Version: (paper in PDF, Iris project page)
This is a significantly revised and expanded synthesis of
our ICFP 2016 and ESOP 2017 papers.
Recipient of 2023 Alonzo Church Award for Outstanding Contributions to Logic and Computation.
-
MoSeL: A General, Extensible Modal Framework for Interactive Proofs in Separation Logic.
Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti,
Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, Derek Dreyer.
In 2018 ACM SIGPLAN International Conference on Functional Programming (ICFP 2018).
Final Version: (paper in PDF, website with Coq development)
Official Citation: PACMPL 2, ICFP, Article 77, September 2018.
-
Mtac2: Typed Tactics for Backward Reasoning in Coq.
Jan-Oliver Kaiser, Beta Ziliani, Robbert Krebbers, Yann Régis-Gianas, Derek Dreyer.
In 2018 ACM SIGPLAN International Conference on Functional Programming (ICFP 2018).
Final Version: (paper in PDF, website with Coq development)
Official Citation: PACMPL 2, ICFP, Article 78, September 2018.
-
RustBelt: Securing the Foundations of the Rust Programming Language.
Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, Derek Dreyer.
In 2018 ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2018).
Final Version: (paper in PDF, website with appendix and Coq development)
Official Citation: PACMPL 2, POPL, Article 66, January 2018.
2017:
-
Robust and Compositional Verification of Object Capability Patterns.
David Swasey, Deepak Garg, Derek Dreyer.
In 2017 ACM SIGPLAN International Conference on Object-Oriented Programming,
Systems, Languages, and Applications (OOPSLA 2017).
Recipient of OOPSLA 2017 Distinguished Paper Award.
Final Version + Appendix: (paper in PDF, Coq development)
Official Citation: PACMPL 1, OOPSLA, Article 89, October 2017.
-
Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris.
Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, Viktor Vafeiadis.
In 2017 European Conference on Object-Oriented Programming (ECOOP 2017).
Recipient of ECOOP 2017 Distinguished Paper Award.
Conference Version: (paper in PDF, website with Coq development and appendix)
-
Repairing Sequential Consistency in C/C++11.
Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, Derek Dreyer.
In 2017 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017).
Recipient of PLDI 2017 Distinguished Paper Award.
Conference Version + Appendix: (paper in PDF)
-
The Essence of Higher-Order Concurrent Separation Logic.
Robbert Krebbers, Ralf Jung, Aleš Bizjak, Jacques-Henri Jourdan, Derek Dreyer, Lars Birkedal.
In 2017 European Symposium on Programming (ESOP 2017).
Conference Version: (paper in PDF, Iris 3.0 documentation, Iris project webpage)
Recipient of 2023 Alonzo Church Award for Outstanding Contributions to Logic and Computation.
-
A Promising Semantics for Relaxed-Memory Concurrency.
Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, Derek Dreyer.
In 2017 ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017).
Conference Version + Appendix: (abstract, paper in PDF, Coq development)
2016:
-
Higher-Order Ghost State.
Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer.
In 2016 ACM SIGPLAN International Conference on Functional Programming (ICFP 2016).
Conference Version: (abstract, paper in PDF, appendices and Coq development, Iris project webpage)
Recipient of 2023 Alonzo Church Award for Outstanding Contributions to Logic and Computation.
-
Lightweight Verification of Separate Compilation.
Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis.
In 2016 ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016).
Conference Version: (abstract, paper in PDF, SepCompCert project webpage with Coq development)
2015:
-
Pilsner: A Compositionally Verified Compiler for a Higher-Order Imperative Language.
Georg Neis, Chung-Kil Hur, Jan-Oliver Kaiser, Craig McLaughlin, Derek Dreyer, Viktor Vafeiadis.
In 2015 ACM SIGPLAN International Conference on Functional Programming (ICFP 2015).
Conference Version: (abstract, paper in PDF, appendix, Coq development)
-
Mtac: A Monad for Typed Tactic Programming in Coq.
Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis.
In Journal of Functional Programming (JFP), Volume 25, e12, July 2015.
Special issue devoted to selected papers from ICFP 2013.
Journal Version: (abstract, paper in PDF, website with Coq development and tutorial)
This is a
significantly revised and expanded version of
our ICFP 2013 paper.
-
Verifying Read-Copy-Update in a Logic for Weak Memory.
Joseph Tassarotti, Derek Dreyer, Viktor Vafeiadis.
In 2015 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2015).
Conference Version: (abstract,
paper in PDF, website with appendix, video abstract)
-
Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning.
Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, Derek Dreyer.
In 2015 ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2015).
Conference Version: (abstract,
paper in PDF, appendix, Iris project webpage)
Recipient of 2023 Alonzo Church Award for Outstanding Contributions to Logic and Computation.
2014:
-
GPS: Navigating Weak Memory with Ghosts, Protocols, and Separation.
Aaron Turon, Viktor Vafeiadis, Derek Dreyer.
In
2014 ACM SIGPLAN International Conference on Object-Oriented Programming,
Systems, Languages, and Applications (OOPSLA 2014).
Conference Version: (abstract, paper in PDF, full version with appendix, website with Coq development)
-
F-ing Modules.
Andreas Rossberg, Claudio Russo, Derek Dreyer.
In Journal of Functional Programming (JFP), 24(5): 529–607, September 2014.
Journal Version: (abstract, paper in PDF, Coq development)
This is a
significantly revised and expanded version of
our TLDI 2010 paper.
-
A Logical Step Forward in Parametric Bisimulations.
Chung-Kil Hur, Georg Neis, Derek Dreyer, Viktor Vafeiadis.
Technical Report MPI-SWS-2014-003, January 2014.
Technical Report: (abstract, paper in PDF, website with Coq development)
-
Backpack: Retrofitting Haskell with Interfaces.
Scott Kilpatrick, Derek Dreyer, Simon Peyton Jones, Simon Marlow.
In 2014 ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2014).
Conference Version: (abstract, paper in PDF, appendix)
2013:
-
Mtac: A Monad for Typed Tactic Programming in Coq.
Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis.
In 2013 ACM SIGPLAN International Conference on Functional Programming (ICFP 2013).
Conference Version: (abstract, paper in PDF, website with Coq development and tutorial)
Talk Slides: (PDF)
This paper is superseded by the journal version cited above.
-
Unifying Refinement and Hoare-Style Reasoning in a Logic for Higher-Order Concurrency.
Aaron Turon, Derek Dreyer, Lars Birkedal.
In 2013 ACM SIGPLAN International Conference on Functional Programming (ICFP 2013).
Conference Version: (abstract, paper in PDF, appendix)
-
Internalizing Relational Parametricity in the Extensional Calculus of Constructions.
Neelakantan R. Krishnaswami, Derek Dreyer.
In 2013 EACSL Annual Conference on Computer Science Logic (CSL 2013).
Conference Version: (abstract, paper in PDF, appendix)
-
How to Make Ad Hoc Proof Automation Less Ad Hoc.
Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, Derek Dreyer.
In Journal of Functional Programming (JFP), 23(4): 357–401, July 2013.
Special issue devoted to selected papers from ICFP 2011.
Journal Version: (abstract, paper in PDF, Coq development)
This is a
significantly revised and expanded version of
our ICFP 2011 paper.
-
Mixin' Up the ML Module System.
Andreas Rossberg, Derek Dreyer.
In ACM Transactions on Programming Languages and Systems (TOPLAS), 35(1), Article 2, April 2013.
Journal Preprint (author-prepared): (abstract, paper in PDF)
This is a significantly revised, corrected and expanded version of our ICFP 2008 paper.
Since the official published version of this article was subject to poor copy
editing,
we ask that you download our author-prepared version instead.
-
Logical Relations for Fine-Grained Concurrency.
Aaron Turon, Jacob Thamsborg, Amal Ahmed, Lars Birkedal, Derek Dreyer.
In 2013 ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2013).
Conference Version: (abstract, paper in PDF, appendix)
-
The Power of Parameterization in Coinductive Proof.
Chung-Kil Hur, Georg Neis, Derek Dreyer, Viktor Vafeiadis.
In 2013 ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2013).
Conference Version: (abstract, paper in PDF, Coq development, Paco library page)
2012:
-
Superficially Substructural Types.
Neelakantan R. Krishnaswami, Aaron Turon, Derek Dreyer, Deepak Garg.
In 2012 ACM SIGPLAN International Conference on Functional Programming (ICFP 2012).
Conference Version: (abstract, paper in PDF, appendix)
-
The Impact of Higher-Order State and Control Effects on Local Relational Reasoning.
Derek Dreyer, Georg Neis, Lars Birkedal.
In Journal of Functional Programming (JFP), 22(4&5): 477–528, September 2012.
Special issue devoted to selected papers from ICFP 2010.
Journal Version: (abstract, paper in PDF, errata, technical appendix)
This is a significantly revised and expanded version of our ICFP 2010 paper.
The technical appendix is citable as Technical Report MPI-SWS-2012-001, April 2012.
-
The Transitive Composability of Relation Transition Systems.
Chung-Kil Hur, Georg Neis, Derek Dreyer, Viktor Vafeiadis.
Technical Report MPI-SWS-2012-002, May 2012.
Technical Report: (abstract, paper in PDF, Coq development)
-
The Marriage of Bisimulations and Kripke Logical Relations.
Chung-Kil Hur, Derek Dreyer, Georg Neis, Viktor Vafeiadis.
In 2012 ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2012).
Conference Version: (abstract, paper in PDF, appendix, Coq development)
Talk Slides: (PDF)
Talk Video: (MP4, ~200 MB)
2011:
-
How to Make Ad Hoc Proof Automation Less Ad Hoc.
Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, Derek Dreyer.
In 2011 ACM SIGPLAN International Conference on Functional Programming (ICFP 2011).
Conference Version: (abstract, paper in PDF, Coq development and appendix)
Talk Slides: (PDF)
This paper is superseded by the JFP version cited above.
-
Non-Parametric Parametricity.
Georg Neis, Derek Dreyer, Andreas Rossberg.
In Journal of Functional
Programming (JFP), 21(4&5): 497–562, September 2011.
Special issue devoted to selected papers from ICFP 2009.
Journal Version: (abstract, paper in PDF)
This is a significantly revised and expanded version of our ICFP 2009 paper.
-
Separation Logic in the Presence of Garbage Collection.
Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis.
In 2011 IEEE Symposium on Logic in Computer Science (LICS 2011).
Conference Version: (abstract, paper in PDF, appendix)
Talk Slides: (PDF)
-
Logical Step-Indexed Logical Relations.
Derek Dreyer, Amal Ahmed, Lars Birkedal.
In Logical Methods in Computer Science (LMCS), 7(2:16): 1–37, June 2011.
Special issue devoted to selected papers from LICS 2009.
Journal Version: (abstract, paper in PDF)
This is a significantly revised, corrected and expanded version of our LICS 2009 paper.
-
A Kripke Logical Relation Between ML and Assembly.
Chung-Kil Hur, Derek Dreyer.
In 2011 ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2011).
Conference Version: (abstract, paper in PDF, appendix)
2010:
2009:
-
Non-Parametric Parametricity.
Georg Neis, Derek Dreyer, Andreas Rossberg.
In 2009 ACM SIGPLAN International Conference on Functional Programming (ICFP 2009).
Conference Version: (abstract,
paper in PDF)
Long Version: (Georg Neis's master's thesis)
This paper is superseded by the JFP version cited above.
-
Logical Step-Indexed Logical Relations.
Derek Dreyer, Amal Ahmed, Lars Birkedal.
In 2009 IEEE Symposium on Logic in Computer Science (LICS 2009).
Conference Version + Appendix: (abstract,
paper in PDF)
Talk Slides: (PDF)
This paper suffers from a non-negligible (if ultimately minor) technical flaw.
It is superseded by the LMCS version cited above.
-
State-Dependent Representation Independence.
Amal Ahmed, Derek Dreyer, Andreas Rossberg.
In 2009 ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2009).
Conference Version:
(abstract,
paper in PDF,
appendix)
2008:
2007:
-
A Type System for Recursive Modules.
Derek Dreyer.
In 2007 ACM SIGPLAN International Conference on Functional Programming (ICFP 2007).
Conference Version:
(abstract,
paper in PDF)
University of Chicago Comp. Sci. Dept. Technical Report TR-2007-10, July 2007.
Technical Report:
(paper in PDF)
-
Recursive Type Generativity.
Derek Dreyer.
In Journal of Functional
Programming (JFP), 17(4&5): 433–471, July & September 2007.
Special issue devoted to selected papers from ICFP 2005.
Journal Version:
(abstract, paper in PDF)
This is a significantly revised and expanded version of my ICFP 2005 paper.
-
Principal Type Schemes for Modular Programs.
Derek Dreyer, Matthias Blume.
In 2007 European Symposium on Programming (ESOP 2007).
Conference Version:
(abstract,
paper in PDF)
Talk Slides: (PPT)
University of Chicago Comp. Sci. Dept. Technical Report TR-2007-02, January 2007.
Supersedes TR-2006-08, October 2006.
Technical Report:
(paper in PDF)
-
Modular Type Classes.
Derek Dreyer, Robert Harper, Manuel M.T. Chakravarty.
In 2007 ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2007).
Conference Version:
(abstract,
paper in PDF)
Talk Slides: (PPT)
University of Chicago Comp. Sci. Dept. Technical Report TR-2006-09, October 2006.
Supersedes TR-2006-03, April 2006.
Technical Report:
(paper in PDF)
2006:
-
Practical Type Theory for Recursive Modules.
Derek Dreyer.
University of Chicago Comp. Sci. Dept. Technical Report TR-2006-07, August 2006.
Technical Report:
(abstract,
paper in PDF)
2005:
-
Recursive Type Generativity.
Derek Dreyer.
In 2005 ACM SIGPLAN International Conference on Functional Programming (ICFP 2005).
Conference Version:
(abstract,
paper in PDF)
Talk Slides: (PPT)
This paper is superseded by the JFP version cited above.
-
Understanding and Evolving the ML Module System.
Derek Dreyer.
PhD Thesis, CMU Technical Report CMU-CS-05-131, May 2005.
Technical Report:
(abstract,
thesis in PDF)
2004:
-
A Type System for Well-Founded Recursion.
Derek Dreyer.
In 2004 ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2004).
Conference Version:
(abstract,
paper in PDF)
Talk Slides: (PPT)
Technical Report: (paper in PDF)
2003:
-
A Type System for Higher-Order Modules.
Derek Dreyer, Karl Crary, Robert Harper.
In
2003 ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2003).
Conference Version:
(abstract,
paper in PDF)
Talk Slides: (PPT)
Technical Report: (paper in PDF)
-
Typed Compilation of Recursive Datatypes.
Joseph C. Vanderwaart, Derek Dreyer, Leaf Petersen,
Karl Crary, Robert Harper, Perry Cheng.
In 2003
ACM SIGPLAN Workshop on Types in Language Design and Implementation
(TLDI 2003).
Conference Version:
(abstract,
paper in PDF)
Talk Slides: (PPT)
Technical Report: (paper in PDF)
2001:
-
Toward a Practical Type Theory for Recursive Modules.
Derek R. Dreyer, Robert Harper, Karl Crary.
CMU Technical Report CMU-CS-01-112, March 2001.
Technical Report:
(abstract,
paper in PDF)
1998:
-
Two Heuristics for the Euclidean Steiner Tree Problem.
Derek R. Dreyer, Michael L. Overton.
Journal of Global Optimization, 13: 95-106, 1998.
Journal Version:
(abstract,
paper in PDF)
Derek Dreyer
Imprint
/ Data
Protection