Modular Reasoning about Concurrent Higher-Order Imperative Programs (ModuRes)
Over the last five years, mainstream programming languages such as
Java, C#, and Scala have evolved to permit a powerful combination of
language features: (a) mutable shared data structures, (b)
higher-order functions, and (c) concurrency. These features are all
very important for programming in practice. However, the combination
of them makes it difficult to write correct and secure programs, and
it is therefore very important to develop mathematically-based
techniques for formal reasoning about correctness and security of
programs with these features.
To get scalable methods that apply to realistic programs, it is
crucial that the mathematical models and logics support modular
reasoning, meaning that specifications and proofs can concentrate on
the resources that a program actually acts upon, instead of its entire
state.
The advent of separation logic has made it easier to reason modularly
about first-order programs with shared mutable data (feature a).
Building on the initial work on separation logic and on relational
models for reasoning about program equivalence, there has recently
been progress on (1) models and logics for modular reasoning about
sequential imperative programs with higher-order functions (features
a, b), and (2) models and logics for modular reasoning about low-level
concurrent imperative programs (features a, c).
The ModuRes project will break new ground by developing mathematical
models and logics for modular reasoning about programs written in
realistic programming languages with all the challenging features (a,
b, c). The project will lay the foundation for future software tools,
which will be used to improve software practice.
The project will be led by Professor Lars Birkedal at Aarhus
University, and will involve international collaboration with the PI's
exceptionally strong network of international collaborators. The
ModuRes project starts in the summer of 2013 and will run for five
years. It is generously funded by
an Advanced
Sapere Aude Grant
from the Danish Council for Independent Research for the Natural Sciences
(FNU).
We are looking for PhD students and postdocs. Please email
Lars Birkedal for information.
Postdocs and PhD students at Aarhus
Former Postdocs and PhD students at Aarhus
Tutorial Material
Iris Project
Selected Related Publications:
[1]R. Jung, R. Krebbers, J-H.
Jourdan, A. Bizjak, L. Birkedal, and D. Dreyer.
Iris from the ground up: A modular foundation for higher-order
concurrent separation logic.
Submitted for publication, 2017.
(PDF)
[2]L. Skorstengaard,
D. Devriese, and L. Birkedal.
Reasoning about a capability machine with local capabilities: Provably
safe stack and return pointer management (without OS support).
2017.
Submitted for publication.
(PDF)
[3]A. Timany, L. Stefanesco,
M. Krogh-Jespersen, and L. Birkedal.
A logical relation for monadic encapsulation of state: Proving
contextual equivalences in the presence of runST.
2017.
Submitted for publication.
[4]A. Bizjak and L. Birkedal.
On models of higher-order separation logic.
In Proceedings of MFPS2017, 2017.
(PDF)
[5]R. Krebbers, R. Jung, A. Bizjak,
J.-H. Jourdan, D. Dreyer, and L. Birkedal.
The essence of higher-order concurrent separation logic.
In Proceedings of ESOP 2017, 2017.
(PDF)
[6]T. Dinsdale-Young, P. Pinto, K.J.
Andersen, and L. Birkedal.
Caper: Automatic verification for fine-grained concurrency.
In Proceedings of ESOP 2017, 2017.
(PDF)
[7]M. Krogh-Jespersen,
K. Svendsen, and L. Birkedal.
A relational model of types-and-effects in higher-order concurrent
separation logic.
In Proceedings of POPL 2017, 2017.
(PDF)
[8]R. Krebbers, A. Timany, and
L. Birkedal.
Interactive proofs in higher-order concurrent separation
logic.
In Proceedings of POPL 2017, 2017.
(PDF)
[9]L. Birkedal, A. Bizjak,
R. Clouston, H.B. Grathwohl, B. Spitters, and A. Vezzosi.
Guarded cubical type theory: Path equality for guarded
recursion.
In Proceedings of CSL 2016 (accepted for publication), 2016.
(PDF)
[10]R. Jung, R. Krebbers,
L. Birkedal, and D. Dreyer.
Higher-order ghost state.
In Proceedings of ICFP 2016, 2016.
(PDF)
[11]A. Bizjak and
L. Birkedal.
A model of guarded recursion via generalised equilogical
spaces.
2016.
Accepted for Publication in TCS.
(PDF)
[12]R. Clouston,
A. Bizjak, H. Bugge Grathwohl, and L. Birkedal.
The guarded lambda calculus: Programming and reasoning with guarded
recursion for coinductive types.
Logical Methods in Computer Science, 2016.
Accepted for publication (journal version of FOSSACS 2015 paper).
(PDF)
[13]L. Birkedal, G. Jaber,
F. Sieczkowski, and J. Thamsborg.
A Kripke logical relation for effect-based program
transformations.
Information and Computation, 2016.
Accepted for publication.
(PDF)
[14]L. Birkedal, A. Bizjak,
R. Clouston, H.B. Gratwohl, B. Spitters, and A. Vezzosi.
Guarded cubical type theory.
In Proceedings of Types 2016, 2016.
(PDF)
[15]K. Svendsen, F. Sieczkowski, and
L. Birkedal.
Transfinite step-indexing: Decoupling concrete and logical
steps.
In Proceedings of ESOP 2016, 2016.
(PDF)
[16]A. Bizjak, H.B. Grathwohl,
R. Clouston, R.E. Møgelberg, and L. Birkedal.
Guarded dependent type theory with coinductive types.
In Proceedings of FOSSACS 2016, 2016.
(PDF)
[17]D. Devriese,
F. Piessens, and L. Birkedal.
Reasoning about object capabilities with logical relations and effect
parametricity.
In Proceedings of EuroS&P 2016, 2016.
(PDF)
[18]D. Devriese,
F. Piessens, and L. Birkedal.
Reasoning about object capabilities with logical relations and effect
parametricity (technical report including proofs and details).
Technical Report CW 690, KU Leuven, January 2016.
(PDF)
[19]M. Dodds, S. Jagannathan, M.J.
Parkinson, K. Svendsen, and L. Birkedal.
Verifying custom synchronisation constructs using higher-order
separation logic.
ACM Transactions on Programming Languages and Systems (TOPLAS),
38(2:4), 2016.
(PDF)
[20]M. Paviotti, R.E. Møgelberg,
and L. Birkedal.
A model of PCF in guarded type theory.
In Proocedings of MFPS, 2015.
(PDF)
[21]F. Sieczkowski, A. Bizjak,
and L. Birkedal.
ModuRes: a Coq library for modular reasoning about concurrent
higher-order imperative programming languages.
In Proceedings of ITP, 2015.
(PDF)
[22]A. Bizjak and
L. Birkedal.
Step-indexed logical relations for probability.
In Proceedings of FOSSACS, 2015.
(PDF)
[23]R. Clouston, A. Bizjak,
H. Bugge Grathwohl, and L. Birkedal.
Programming and reasoning with guarded recursion for coinductive
types.
In Proceedings of FOSSACS, 2015.
(PDF)
[24]F. Sieczkowski, K. Svendsen,
L. Birkedal, and J. Pichon-Pharapod.
A separation logic for fictional sequential consistency.
In Proceedings of ESOP, 2015.
(PDF)
[25]R. Jung, D. Swasey,
F. Sieczkowski, K. Svendsen, A. Turon, L. Birkedal, and D. Dreyer.
Iris: Monoids and invariants as an orthogonal basis for concurrent
reasoning.
In Proceedings of POPL, 2015.
(PDF)
[26]A. Bizjak,
L. Birkedal, and M. Miculan.
A model of countable nondeterminism in guarded type theory.
In Proceedings of TLCA, 2014.
(PDF)
[27]K. Svendsen and L. Birkedal.
Impredicative Concurrent Abstract Predicates.
In Proceedings of ESOP, 2014.
(PDF)
[28]L. Birkedal, A. Bizjak,
and J. Schwinghammer.
Step-indexed relational reasoning for countable
nondeterminism.
Logical Methods in Computer Science, 9(4):1-23, October 2013.
lmcs online version.
(PDF)
[29]A. Turon, D. Dreyer, and
L. Birkedal.
Unifying refinement and hoare-style reasoning in a logic for
higher-order concurrency.
In Proceedings of ICFP, 2013.
(PDF)
[30]L. Birkedal and R.E.
Møgelberg.
Intensional type theory with guarded recursive types qua fixed points
on universes.
In Proceedings of LICS, 2013.
(PDF)
[31]K. Svendsen, L. Birkedal, and
M. Parkinson.
Joins: A case study in modular specification of a concurrent reentrant
higher-order library.
In Proceedings of ECOOP, 2013.
(PDF)
[32]K. Svendsen, L. Birkedal, and
M. Parkinson.
Modular reasoning about separation of concurrent data
structures.
In Proceedings of ESOP, 2013.
(PDF)
[33]Lars Birkedal and Ales Bizjak.
A note on the transitivity of step-indexed logical relations.
Manuscript, November 2012.
(PDF)
[34]A. Turon, J. Thamsborg,
A. Ahmed, L. Birkedal, and D. Dreyer.
Logical relations for fine-grained concurrency.
In Proceedings of POPL, January 2013.
(PDF)
[35]T. Dinsdale-Young, L. Birkedal,
P. Gardner, M. Parkinson, and H. Yang.
Views: Compositional reasoning for concurrency.
In Proceedings of POPL, January 2013.
(PDF)
[36]L. Birkedal, R. Møgelberg,
J. Schwinghammer, and K. Støvring.
First steps in synthetic guarded domain theory: step-indexing in the
topos of trees.
Logical Methods in Computer Science, 8(4), October 2012.
lmcs online version.
(PDF)
[37]J. Thamsborg,
L. Birkedal, and H. Yang.
Two for the price of one: Lifting separation logic assertions.
Logical Methods in Computer Science, 8(3), September 2012.
lmcs online version.
(PDF)
[38]L. Birkedal, F. Sieczkowski, and
J. Thamsborg.
A concurrent logical relation.
In Proceedings of CSL, September 2012.
(PDF)
[39]J. Bengtson, J.B. Jensen, and
L. Birkedal.
Charge! a framework for higher-order separation logic in
Coq.
In Proceedings of ITP, August 2012.
(PDF)
[40]L. Birkedal, K. Støvring, and
J. Thamsborg.
A relational realizability model for higher-order stateful
ADTs.
Journal of Logic and Algebraic Programming, 81(4):491-521,
January 2012.
(PDF)
[41]D. Dreyer, G. Neis, and
L. Birkedal.
The impact of higher-order state and control effects on local
relational reasoning.
Journal of Functional Programming, February 2012.
To Appear (accepted for publication).
(PDF)
[42]J. Schwinghammer,
L. Birkedal, F. Pottier, B. Reus, K. Støvring, and H. Yang.
A step-indexed Kripke model of hidden state.
Mathematical Structures in Computer Science, 2012.
(To Appear. Accepted for publication).
(PDF)
[43]J.B. Jensen and L. Birkedal.
Fictional separation logic.
In Proceedings of ESOP 2012, 2012.
(PDF)
[44]H. Mehnert, F. Sieczkowski,
L. Birkedal, and P. Sestoft.
Formalized verification of snapshotable trees: Separation and
sharing.
In Proceedings of VSTTE 2012, 2012.
(PDF)