Two possible rewritings of the central structure in a proof search
Two possible rewritings of the central structure in a proof search
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.
Bath:
Torino:
A Deep Inference System with a Self-Dual Binder Which Is Complete for Linear Lambda Calculus
Luca Roversi
Abstract We recall that SBV, a proof system developed under the methodology of deep inference, extends multiplicative linear logic with the self-dual non-commutative logical operator Seq. We introduce SBVB that extends SBV by adding the self-dual binder Sdb on names. The system SBVB is consistent because we prove that (the analogous of) cut-elimination holds for it. Moreover, the resulting interplay between Seq and Sdb can model β-reduction of linear λ-calculus inside the cut-free subsystem BVB of SBVB. The long term aim is to keep developing a programme whose goal is to give pure logical accounts of computational primitives under the proof-search-as-computation analogy, by means of minimal and incremental extensions of SBV.
Pdf 25 January 2014
To appear on Journal of Logic and Computation
Communication, and Concurrency with Logic-Based Restriction Inside a Calculus of Structures
Luca Roversi
Abstract It is well known that we can use structural proof theory to refine, or generalize, existing paradigmatic computational primitives, or to discover new ones. Under such a point of view we keep developing a programme whose goal is establishing a correspondence between proof-search of a logical system and computations in a process algebra. We give a purely logical account of a process algebra operation which strictly includes the behavior of restriction on actions we find in Milner CCS. This is possible inside a logical system in the Calculus of Structures of Deep Inference endowed with a self-dual quantifier. Using proof-search of cut-free proofs of such a logical system we show how to solve reachability problems in a process algebra that subsumes a significant fragment of Milner CCS.
Pdf 19 December 2012
Submitted
10–15.9.12 Paolini and Roversi visit Bath, Tom Gundersen and Michel Parigot join coming from Paris (PPS). Roversi talks about Concurrency and Communication with Restriction in Deep Inference and Gundersen talks about An Explicit Sharing Lambda Calculus.
23–27.3.13 Roversi visits Bath to discuss BV models.
9–13.9.13 Guglielmi visits Torino to discuss BV models.
17–21.2.14 Bruscoli visits Torino to discuss BV models.
13–15.5.14 Berardi, Cardone, Paolini, Piccolo and Roversi visit Bath to participate in the Sharing and Sequentiality in Proof Systems with Locality workshop.
15–18.6.14 Duchesne and Heijltjes visit Torino. Heijltjes talks about The Atomic Lambda Calculus.
30.6.2014 Alessio Guglielmi email
