https://www.ins2i.cnrs.fr/en/cnrsin...
There remains a strong and ongoing need in the development, design, and semantics of programming languages to provide the most contextually appropriate abstractions possible. This is particularly valuable for producing compilers and mechanized verification tools. For instance, one might consider programming languages like Rust, which offers safe yet optimized memory management, making it suitable for systems programming applications. Alternatively, domain-specific languages for parallelism can bridge the gap between deterministic specifications and target embedded code capable of running on parallel architectures (e.g., multi-core systems). In most cases, these abstractions are achieved through the design of novel type systems, whose properties are formally proven. Exploiting these systems requires the development of modern compilation and verification techniques to generate code that is both safe and efficient. These research themes are actively explored by communities that publish in conferences such as POPL, PLDI, ICFP, OOPSLA, and ECOOP.
