Software Science

Writing a small computer program is easy. Designing and producing a complete software program that is reliable, durable and resistant to attack remains extraordinarily difficult. It is the aim of Software Science to design and develop the principles, mathematical formalisms, empirical techniques and computational tools needed to design, program and verify reliable, secure software.

The Software Science lectures aim to explore these issues and present contemporary research in the field. The lecture focuses on approaches known as " formal ", as opposed to the empiricism often used in software engineering. These approaches are based on known or emerging mathematically rigorous foundations : formal semantics, program logic, deductive systems, program equivalence, process calculus... Historically, these concepts emerged from very down-to-earth programming considerations before being adorned with mathematical rigor. The lecture traces this progression of ideas from the programmer's intuition to the mechanization of these formal approaches.

The first years of this lecture could have been entitled " Programming, demonstrating ", as they explored several modes of interaction between software programming and the demonstration of mathematical statements : programming then demonstrating, as in program logics for deductive verification ; programming to demonstrate, as in constructive logics and the Coq demonstration assistant ; finally, programming equals demonstrating, as in the fruitful Curry-Howard correspondence, the subject of the first year of the lecture. Subsequent years explore other facets of Software Science, notably the comparative study of programming languages and software security, through " languages " or cryptographic approaches.

The Software Science Chair's research is carried out within the framework of the Cambiumproject-team , a joint venture with Inria. The team's work aims to improve the reliability, safety and security of software by advancing programming languages and formal program verification methods. The main research themes are deductive program verification, type systems and type inference algorithms, and shared-memory parallelism. The team designs and develops two major research software packages that integrate and translate many of its results into practice : OCaml, a statically typed functional programming language and its implementation, and CompCert, a formally verified compiler for mission-critical embedded software. In 2021, CompCert received the ACM Software System Award, the highest distinction for research-based software.