Derek Dreyer

From MaRDI portal
Person:1265186

Available identifiers

zbMath Open dreyer.derek-rMaRDI QIDQ1265186

List of research outcomes





PublicationDate of PublicationType
Local reasoning about the presence of bugs: incorrectness separation logic2021-02-09Paper
Iris from the ground up: a modular foundation for higher-order concurrent separation logic2019-02-20Paper
Mtac: a monad for typed tactic programming in Coq2017-10-23Paper
A promising semantics for relaxed-memory concurrency2017-10-20Paper
The essence of higher-order concurrent separation logic2017-05-19Paper
Higher-order ghost state2017-05-10Paper
Pilsner: a compositionally verified compiler for a higher-order imperative language2017-05-10Paper
Internalizing relational parametricity in the extensional calculus of constructions2017-02-02Paper
Lightweight verification of separate compilation2016-10-24Paper
Iris: monoids and invariants as an orthogonal basis for concurrent reasoning2016-09-29Paper
A type system for well-founded recursion2015-11-11Paper
The marriage of bisimulations and Kripke logical relations2015-09-11Paper
A type system for higher-order modules2015-09-11Paper
State-dependent representation independence2015-07-03Paper
A relational modal logic for higher-order stateful ADTs2015-06-11Paper
Mtac: a monad for typed tactic programming in Coq2015-03-30Paper
Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency2015-03-30Paper
F-ing modules2015-03-25Paper
Mixin' up the ML module system2015-03-16Paper
The impact of higher-order state and control effects on local relational reasoning2015-03-05Paper
How to make ad hoc proof automation less ad hoc2015-03-05Paper
Recursive type generativity2015-01-06Paper
Non-parametric parametricity2015-01-06Paper
The power of parameterization in coinductive proof2014-11-27Paper
Logical relations for fine-grained concurrency2014-11-27Paper
Modular type classes2014-09-12Paper
A type system for recursive modules2014-07-21Paper
Superficially substructural types2014-07-21Paper
Backpack, retrofitting Haskell with interfaces2014-04-10Paper
A Kripke logical relation between ML and assembly2014-04-10Paper
How to make ad hoc proof automation less ad hoc2014-02-27Paper
Non-parametric parametricity2013-04-24Paper
The impact of higher-order state and control effects on local relational reasoning2012-10-29Paper
Recursive type generativity2007-09-26Paper
Principal Type Schemes for Modular Programs2007-09-04Paper
Two heuristics for the Euclidean Steiner tree problem1998-01-01Paper

Research outcomes over time

This page was built for person: Derek Dreyer