Modular Reasoning about Concurrent Higher-Order Imperative Programs (ModuRes)

ModuRes_logo

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)