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.
K. Svendsen, L. Birkedal, and A. Nanevski. Partiality, state, and dependent types. February 2011. Submitted for publication. (PDF, 230531 bytes)
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. January 2011. Submitted for publication. (PDF, 344599 bytes)
A. Ahmed, N. Benton, L. Birkedal, and M. Hofmann. Modelling, Controlling, and Reasoning about State. Seminar Proceedings, Executive Summary and Abstracts Collection. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany 2010., 2010.
J. Schwinghammer, L. Birkedal, and K. Støvring. A step-indexed kripke model of hidden state via recursive properties on recursively defined metric spaces. October 2010. Accepted for publication in FOSSACS 2011. (PDF, 566705 bytes)
L. Birkedal, B. Reus, J. Schwinghammer, K. Støvring, J. Thamsborg, and H. Yang. Step-indexed kripke models over recursive worlds. 2010. Accepted for publication at POPL 2011. (PDF, 431059 bytes)
L. Birkedal, K. Støvring, and J. Thamsborg. The category-theoretic solution of recursive metric-space quations. Theoretical Computer Science, 411:4102-4122, 2010. (PDF, 517809 bytes)
N. Benton, L. Birkedal, A. Kennedy, and C. Varming. Formalizing domains, ultrametric spaces and semantics of programming languages. 2010. Submitted for publication. Coq Script: domultracoq.zip . (PDF, 874071 bytes)
L. Birkedal, J. Schwinghammer, and K. Støvring. A step-indexed kripke model of hidden state via recursive properties on recursively defined metric spaces. 2010. Presented at FICS 2010. (PDF, 224826 bytes)
L. Birkedal, J. Schwinghammer, and K. Støvring. A metric model of guarded recursion. 2010. Presented at FICS 2010. (PDF, 159942 bytes)
L. Birkedal, K. Støvring, and J. Thamsborg. Realizability semantics of parametric polymorphism, general references, and recursive types. Mathematical Structures in Computer Science, May 2010. To Appear (accepted for publication). (PDF, 402237 bytes)
D. Dreyer, G. Neis, and L. Birkedal. The impact of higher-order state and control effects on local relational reasoning. In Proc. of ICFP 2010, 2010. (PDF, 247566 bytes)
J.B. Jensen, L. Birkedal, and P. Sestoft. Modular verification of linked lists with views via separation logic. 2010. Presented at FTfJP'2010. (PDF, 321793 bytes)
L. Birkedal, K. Støvring, and J. Thamsborg. A relational realizability model for higher-order stateful ADTs. March 2010. Submitted for publication. (PDF, 378294 bytes)
J. Thamsborg, L. Birkedal, and H. Yang. Two for the price of one: Lifting separation logic assertions. January 2010. Manuscript. (PDF, 284124 bytes)
K. Svendsen, L. Birkedal, and M. Parkinson. Verifying generics and delegates. December 2009. Accepted for publication in ECOOP 2010. (PDF, 271959 bytes)
L. Birkedal, K. Støvring, and J. Thamsborg. Realizability semantics of parametric polymorphism, general references, and recursive types. Technical Report TR-2010-124, IT University of Copenhagen, jan 2010. (PDF, 454483 bytes)
J. Schwinghammer, H. Yang, L. Birkedal, F. Pottier, and B. Reus. A semantic foundation for hidden state. In Proceedings of FOSSACS 2010, October 2009. To Appear (accepted for publication). (PDF, 425026 bytes)
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)
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)