OLAS

Le logiciel transforme de plus en plus notre vie quotidienne. Mais les applications deviennent aussi de plus en plus complexes. Cela pose d'énormes défis lorsqu'il s'agit de garantir que les logiciels fonctionnent correctement et efficacement. La correction consiste en garantir qu'un programme répond aux exigences attendues. L'efficacité consiste en mieux contrôler l'utilisation des ressources lors de l'exécution d'un programme, et ce sans affecter le comportement global.

Au sein d'Olas, nous étudions des modèles et des techniques permettant de raisonner sur la correction et sur l'efficacité des systèmes logiciels modernes. Nous nous concentrons sur les langages et les formalismes d'ordre supérieur, au sens où ceux-ci permettent, syntaxiquement ou sémantiquement, la représentation de fonctions générales, y compris des fonctions qui prennent d'autres fonctions comme arguments. Une spécificité des langages d'ordre supérieur est qu'ils sont ouverts : la visibilité qu'un terme a de son environnement peut changer au fil du temps, car l'interaction du terme avec son environnement affectera les capacités futures en termes d'interactions. Une autre caractéristique est la possibilité d'abstraire, à la fois vis-à-vis des données et vis-à-vis du comportement. Les constructions d'ordre supérieur sont importantes dans les langages de programmation de haut niveau modernes. Par exemple, les logiciels sont généralement ouverts car ils s'exécutent en réseau ; et l'abstraction est importante pour écrire du code concis et pour améliorer la modularité. En effet, les langages de programmation modernes incluent normalement des constructions d'ordre supérieur.