CASH

The overall objective of the CASH team is to design and develop ways to improve the quality of software. We work both on tools that help programmers write better programs, and compilers that turn these programs into efficient executables. The scope of targeted applications is wide, from specialized HPC applications on supercomputers to general purpose computing, from massively parallel applications to sequential code, from functional languages to imperative code, etc. Our main focus is software, but we also consider hardware, both as an execution platform for software, and as a research topic (hardware generation and hardware circuit analysis). What links all our activities is that our object of study is computer programs.

By improving the quality, we mean both the safety of programs and the efficiency of their execution. We notably provide programmers with better programming language constructs to express their intent: constructions that give them guarantees by-construction such as memory-safety, determinism, etc. When guarantees can't be obtained by construction, we also develop static analyses to detect bugs or to prove preconditions needed to apply program transformations. We use such guarantees to develop new optimizations to generate efficient code. All these contributions find their foundation and justification in the semantics of programs. Additinally, we provide simulators to execute programs that require a specific execution platform.

When it comes to high level programming constructs for parallelism, we develop a specific expertise in asynchronous computations and ruling out race-conditions in concurrent programs. In this realm, we propose new paradigms, but also contribute to the semantics of such programs. For instance, we design ways to specify the semantics using monadic interpreters, and use them to study the correctness of compilers.

We ensure safety guarantees both through type-systems and analyses, in vastly different contexts: from the verification of electrical circuits to the design of a new module systems for OCaml. As is recurrent in our work, we pragmatically adapt the approach to the practical application at hand.

We design code transformation for the efficient execution of programs, in particular targetting HPC. Our contributions in this realm extend the polyhedral model to make it applicable to a wider range of programs, and to bring its potential for optimisation to new kind of applications (parametric tiling, sparse structures, ...). We also design optimisations for structured data such as trees, or more generally algebraic data types.