Computer systems are nowadays entangled with every aspect of our life. Whereas a few decades ago a ``computer bug'' might have been just a little annoyance, it can be life-threatening today. It is therefore of vital importance to develop a systematic methodology for producing ``bug-free'' software. The task is easier for declarative programming languages than for imperative ones. In particular, functional languages come with a rich tool set helping establishing the correctness of programs. This is mainly due to the successful application of mathematical logic, based on the proofs-as-programs principle (also known as Curry-Howard correspondence) stating that writing a program is basically the same thing as proving a theorem, and the computation of the program is the same a normalizing the proof. This is the basis of all functional programming languages.
The normalization process and its complexity depend on the chosen representation of the proof or program. The standard setting here is the correspondence between terms on the lambda-calculus on one side and proofs in intuitionistic logic on the other side. And in this setting, intuitionistic combinatorial proofs offer a completely new perspective, as they (i) incorporate a form of sharing that is not present in the lambda-calculus, and (ii) form a representation of proofs that it independent from the syntax of proof systems.
In this project we plan to explore the potential of combinatorial proofs in two directions: first, in the theory of functional programming languages, through their normalization behaviour, and second, in the verification of imperative programs, through their representation of proofs in the logic of bunched implications.
Due to the Covid19 crisis, all meetings planned for 2020 have been cancelled.