OLAS

Software is more and more transforming our daily lives. However, it is also becoming more and more complex. This raises tremendous challenges when it comes to ensuring that software works correctly and efficiently. Correctness is about ensuring that a program satisfies expected requirements. Efficiency is about reducing the resource usage of the runs of a program without affecting the overall behaviour.

In Olas we study models and techniques for reasoning about the correctness and efficiency of modern software systems. We focus on languages and formalisms that are higher-order, in that they allow, either syntactically or semantically, the representation of general functions, including functions that take other functions as arguments. A distinctive feature of higher-order languages is open-endedness: the visibility that a term has of its environment may change over time, because the interaction of the term with its environment will affect the future capabilities of interactions. Another feature is abstraction, both on data and on behaviour. Higher-order constructs are important in modern high-level programming languages. For instance, software is typically open-ended because it is connected to the Internet; and abstraction is important for writing concise code and for enhancing modularity. Indeed, modern mainstream programming languages normally include higher-order constructs.