Sharing and Sequentiality in Proof Systems with Locality
Royal Society International Exchanges
1.7.2012–30.6.2014


Two possible rewritings of the central structure in a proof search

1    Summary

While writing and executing programs is relatively straightforward, proving their correctness is still only rarely achieved. We want to contribute to solving the problem of producing provably safe and reliable software by the methods of proof theory.

The idea is to use proof theory's sophisticated tools for manipulating formal mathematical proofs to the advantage of programming. For us, it is especially interesting that a very complicated and somewhat repetitive formal proof can be compressed by recognising the repeating parts, and describing them in detail only once. This is a very similar process to the one used by the ZIP program to compress files.

We can associate the process of unfolding a compressed proof to that of executing a program, and, conversely, compressing a proof can be associated to analysing a computation. The details are a bit more complicated, but this idea captures the essence of what we work on. However, proof theory has been developed for the formal language of mathematics, while computer languages require a much greater expressiveness to be effective. In fact, it would be possible to program computers in the traditional language of mathematics, but this would be terribly inefficient, and it is not done in practice. So, if we want to use proof theory, we have to adapt it to the more expressive languages of computer science.

In this project, we intend to do so by concentrating mainly on two aspects: sharing and sequentiality. Sharing has a lot to do with the compression mechanism mentioned above, and it is about representing data efficiently by avoiding repeating identical chunks of information, and instead pointing to them inside data structures. Sequentiality is the property such that pieces of programs are forced to be executed at different times, because they are in a causal relation: one has to precede the other.

The traditional proof theory of mathematical languages cannot express sharing and sequentiality in an explicit and convenient way. In other words, it is not possible to write proofs and manipulate them in such a way that sharing and sequentiality are explicitly controlled and behave the same as they do in an ordinary computer program.

There has been a recent advance in proof theory, which allows us to represent and manipulate proofs in much finer detail than previously possible. This progress has been made possible by a property called 'locality';. Locality is obtained by exploiting a certain symmetry that had been overlooked in the early days of proof theory (more than 70 years ago). Thanks to locality, sharing and sequentiality, together with several other features of computer languages, are now explicitly controllable in certain logical languages.

The challenge for us is straightforward: can we harness, to the benefit of real computer languages, the power of locality for sharing and sequentiality? The choice of sharing and sequentiality is dictated by their importance in computer languages and by opportunity, given that these aspects intersect the research interests of our teams in Torino and Bath.

We believe that we will be able to establish a stronger connection between computer languages and proof theory, by bringing proof theory and its bag of tools closer to computer languages. This way, we will contribute to the invention of methods and techniques that will allow us to program computers with greater accuracy and at a lesser cost.

Value of this project: 11,960 GBP.

2    People

Bath:

Torino:

3    Papers

4    Activity

    


Electric lamps were not invented by improving candles

      30.6.2014    Alessio Guglielmi    email