Derek Dreyer

Available identifiers

zbMath Open dreyer.derek-rMaRDI QIDQ1265186

List of research outcomes

Publication	Date of Publication	Type
Local reasoning about the presence of bugs: incorrectness separation logic	2021-02-09	Paper
Iris from the ground up: a modular foundation for higher-order concurrent separation logic	2019-02-20	Paper
Mtac: a monad for typed tactic programming in Coq	2017-10-23	Paper
A promising semantics for relaxed-memory concurrency	2017-10-20	Paper
The essence of higher-order concurrent separation logic	2017-05-19	Paper
Higher-order ghost state	2017-05-10	Paper
Pilsner: a compositionally verified compiler for a higher-order imperative language	2017-05-10	Paper
Internalizing relational parametricity in the extensional calculus of constructions	2017-02-02	Paper
Lightweight verification of separate compilation	2016-10-24	Paper
Iris: monoids and invariants as an orthogonal basis for concurrent reasoning	2016-09-29	Paper
A type system for well-founded recursion	2015-11-11	Paper
The marriage of bisimulations and Kripke logical relations	2015-09-11	Paper
A type system for higher-order modules	2015-09-11	Paper
State-dependent representation independence	2015-07-03	Paper
A relational modal logic for higher-order stateful ADTs	2015-06-11	Paper
Mtac: a monad for typed tactic programming in Coq	2015-03-30	Paper
Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency	2015-03-30	Paper
F-ing modules	2015-03-25	Paper
Mixin' up the ML module system	2015-03-16	Paper
The impact of higher-order state and control effects on local relational reasoning	2015-03-05	Paper
How to make ad hoc proof automation less ad hoc	2015-03-05	Paper
Recursive type generativity	2015-01-06	Paper
Non-parametric parametricity	2015-01-06	Paper
The power of parameterization in coinductive proof	2014-11-27	Paper
Logical relations for fine-grained concurrency	2014-11-27	Paper
Modular type classes	2014-09-12	Paper
A type system for recursive modules	2014-07-21	Paper
Superficially substructural types	2014-07-21	Paper
Backpack, retrofitting Haskell with interfaces	2014-04-10	Paper
A Kripke logical relation between ML and assembly	2014-04-10	Paper
How to make ad hoc proof automation less ad hoc	2014-02-27	Paper
Non-parametric parametricity	2013-04-24	Paper
The impact of higher-order state and control effects on local relational reasoning	2012-10-29	Paper
Recursive type generativity	2007-09-26	Paper
Principal Type Schemes for Modular Programs	2007-09-04	Paper
Two heuristics for the Euclidean Steiner tree problem	1998-01-01	Paper

Research outcomes over time

This page was built for person: Derek Dreyer