Inria Équipe Associée 2020–2024

COMPRONOM — Combinatorial Proof Normalization


Scientific Background

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.


Participating teams

Partout team, Inria Saclay - Ile-de-France
Responsible: Lutz Straßburger

Mathematical foundations group, University of Bath
Responsible: Willem Heijltjes

PPLV group, University College London
Responsible: David Pym


Events

(Due to the Covid19 crisis, all meetings planned for 2020 and 2021 have been cancelled.)


Publications

Giti Omidvar and Lutz Straßburger
Combinatorial Flows as Bicolored Atomic Flows
Pdf        September 2022
Presented at WoLLIC 2022
 
Willem Heijltjes and Dominic Hughes and Lutz Straßburger
Normalization without syntax
Pdf        August 2022
In proceedings of FSCD 2022



  Last update:  December 13, 2023            Lutz Straßburger