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 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)