The goal of the MOREASO project is to develop theories and methods for Modular Reasoning about Software written in modern programming languages. The purpose is to lay the foundation for improvement of software tools, which are being and will be developed over the next five to ten years.
The project is funded for three years (starting January 2008) by the Danish Agency for Science, Technology and Innovation (FNU) and by the IT University of Copenhagen.
N. Krishnaswami, L. Birkedal, and J. Aldrich. Verifying event-driven programs using ramified frame properties. In Proceedings of TLDI'2010, 2010. To Appear. (PDF, 287590 bytes)
J. Schwinghammer, H. Yang, L. Birkedal, F. Pottier, and B. Reus. A semantic foundation for hidden state. October 2009. Submitted for publication. (PDF, 425026 bytes)
L. Birkedal, K. Støvring, and J. Thamsborg. The category-theoretic solution of recursive metric-space quations. Technical Report ITU-2009-119, IT University of Copenhagen, 2009. (PDF, 369438 bytes)
D. Dreyer, G. Neis, A. Rossberg, and L. Birkedal. A relational modal logic for higher-order stateful ADTs. July 2009. To Appear in POPL'2010 (accepted for publication). (PDF, 339559 bytes)
L. Birkedal, K. Støvring, and J. Thamsborg. Solutions of generalized recursive metric-space equations. In Proceedings of FICS 2009, September 2009. (PDF, 76433 bytes)
D. Dreyer, A. Ahmed, and L. Birkedal. Logical step-indexed logical relations. In Proceedings of LICS 2009, August 2009. (PDF, 238714 bytes)
J. Schwinghammer, L. Birkedal, B. Reus, and H. Yang. Nested Hoare triples and frame rules for higher-order store. In Proceedings of CSL 2009, April 2009. (PDF, 332572 bytes)
L. Birkedal, K. Støvring, and J. Thamsborg. Realizability semantics of parametric polymorphism, references, and recursive types. In Proceedings of FOSSACS'09, April 2009. To Appear (Accepted for publication). (PDF, 258769 bytes)
L. Birkedal, K. Støvring, and J. Thamsborg. Relational parametricity for references and recursive types. In Proceedings of TLDI, January 2009. (PDF, 255124 bytes)
N. Krishnaswami, J. Aldrich, L. Birkedal, K. Svendsen, and A. Buisse. Design patterns in separation logic. In Proc. of TLDI 2009, January 2009. (PDF, 236270 bytes)
K. Svendsen, A. Buisse, L. Birkedal. Verifying Design Patterns in Hoare Type Theory . Technical report ITU-TR-2008-112, 2008. (PDF)
A. Nanevski, G. Morrisett, A. Shinnar, P. Goverau, and L. Birkedal. Ynot: Dependent types for imperative programs. In Proc. of ICFP 2008, Sep 2008. (PDF, 281368 bytes)
L. Birkedal, B. Reus, J. Schwinghammer, and H. Yang. A Simple Model of Separation Logic for Higher-order Store. In Proceedings of ICALP 2008, 2008. (PDF, 273463 bytes)
C. Varming and L. Birkedal. Higher-order separation logic in Isabelle/HOLCF. In Proceedings of MFPS 2008, 2008. (PDF, 295613 bytes)
R.L. Petersen, L. Birkedal, A. Nanevski, and G. Morrisett. A Realizability Model of Impredicative Hoare Type Theory. In Proceedings of ESOP 2008, 2008. (PDF) Extended version available as technical report.
L. Birkedal and H. Yang. Relational parametricity and separation logic. Logical Methods in Computer Science, 2008. To Appear (accepted for publication). (PDF)
N. Krishnaswami, J. Aldrich, and L. Birkedal. Modular verification of the subject-observer pattern via higher-order separation logic. In 9th Workshop on Formal Techniques for Java-like Programs (FTfJP 2007), 2007. (PDF)
B. Biering, L. Birkedal, and N. Torp-Smith. BI-hyperdoctrines, higher-order separation logic, and abstraction. ACM Transactions on Programming Languages and Systems, 2007. To appear. (PDF)
L. Birkedal and H. Yang. Relational parametricity and separation logic. In Proceedings of FOSSACS 2007, 2007. (PDF)
A. Nanevski, A. Ahmed, G. Morrisett, and L. Birkedal. Abstract predicates and mutable ADTs in Hoare type theory. In Proceedings of ESOP 2007, 2007. (PDF) Extended version avaialable as technical report.
L. Birkedal, R.E. Møgelberg, and R.L. Petersen. Linear Abadi and Plotkin logic. Logical Methods in Computer Science, 2(5:2), August 2006. lmcs online version.
L. Birkedal, N. Torp-Smith, and H. Yang. Semantics of separation-logic typing and higher-order frame rules for algol-like languages. Logical Methods in Computer Science, 2(5:1), August 2006. lmcs online version.
N. Torp-Smith, L. Birkedal, and J.C. Reynolds. Local reasoning about a copying garbage collector. ACM Transactions on Programming Languages and Systems, 2006. To Appear. (PDF)
A. Nanevski, G. Morrisett, and L. Birkedal. Polymorphism and separation in hoare type theory. In Proceedings of ICFP 2006, September 2006. (PDF)
N. Bohr and L. Birkedal. Relational reasoning for recursive types and references. In Proceedings of APLAS 2006, June 2006. (PDF)