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 at Aarhus
Tutorial Material
Selected Related Publications:
[1]K. Svendsen, F. Sieczkowski, and
L. Birkedal.
Transfinite step-indexing: Decoupling concrete and logical
steps.
In Proceedings of ESOP 2016, 2016.
(PDF, 481803 bytes)
[2]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, 377884 bytes)
[3]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, 384568 bytes)
[4]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, 817454 bytes)
[5]R. Clouston,
A. Bizjak, H. Bugge Grathwohl, and L. Birkedal.
The guarded lambda calculus: Programming and reasoning with guarded
recursion for coinductive types.
2015.
Submitted for publications (journal version of FOSSACS 2015 paper).
(PDF, 549867 bytes)
[6]A. Bizjak and
L. Birkedal.
A model of guarded recursion via generalised equilogical
spaces.
2015.
Submitted for publication.
(PDF, 384615 bytes)
[7]M. Dodds, S. Jagannathan, M.J.
Parkinson, K. Svendsen, and L. Birkedal.
Verifying custom synchronisation constructs using higher-order
separation logic.
2015.
Accepted for publication in TOPLAS.
(PDF, 729395 bytes)
[8]M. Paviotti, R.E. Møgelberg,
and L. Birkedal.
A model of PCF in guarded type theory.
In Proocedings of MFPS, 2015.
(PDF, 356835 bytes)
[9]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, 290779 bytes)
[10]A. Bizjak and
L. Birkedal.
Step-indexed logical relations for probability.
In Proceedings of FOSSACS, 2015.
(PDF, 503939 bytes)
[11]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, 489500 bytes)
[12]F. Sieczkowski, K. Svendsen,
L. Birkedal, and J. Pichon-Pharapod.
A separation logic for fictional sequential consistency.
In Proceedings of ESOP, 2015.
(PDF, 480060 bytes)
[13]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, 424511 bytes)
[14]A. Bizjak,
L. Birkedal, and M. Miculan.
A model of countable nondeterminism in guarded type theory.
In Proceedings of TLCA, 2014.
(PDF, 390819 bytes)
[15]K. Svendsen and L. Birkedal.
Impredicative Concurrent Abstract Predicates.
In Proceedings of ESOP, 2014.
(PDF, 388637 bytes)
[16]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, 382294 bytes)
[17]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, 394684 bytes)
[18]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, 322513 bytes)
[19]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, 416977 bytes)
[20]K. Svendsen, L. Birkedal, and
M. Parkinson.
Modular reasoning about separation of concurrent data
structures.
In Proceedings of ESOP, 2013.
(PDF, 418226 bytes)
[21]Lars Birkedal and Ales Bizjak.
A note on the transitivity of step-indexed logical relations.
Manuscript, November 2012.
(PDF, 171003 bytes)
[22]A. Turon, J. Thamsborg,
A. Ahmed, L. Birkedal, and D. Dreyer.
Logical relations for fine-grained concurrency.
In Proceedings of POPL, January 2013.
(PDF, 399228 bytes)
[23]T. Dinsdale-Young, L. Birkedal,
P. Gardner, M. Parkinson, and H. Yang.
Views: Compositional reasoning for concurrency.
In Proceedings of POPL, January 2013.
(PDF, 349684 bytes)
[24]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, 642856 bytes)
[25]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, 284124 bytes)
[26]L. Birkedal, F. Sieczkowski, and
J. Thamsborg.
A concurrent logical relation.
In Proceedings of CSL, September 2012.
(PDF, 643470 bytes)
[27]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, 225313 bytes)
[28]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, 525301 bytes)
[29]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, 895071 bytes)
[30]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, 523089 bytes)
[31]J.B. Jensen and L. Birkedal.
Fictional separation logic.
In Proceedings of ESOP 2012, 2012.
(PDF, 229056 bytes)
[32]H. Mehnert, F. Sieczkowski,
L. Birkedal, and P. Sestoft.
Formalized verification of snapshotable trees: Separation and
sharing.
In Proceedings of VSTTE 2012, 2012.
(PDF, 211400 bytes)