On the Computational Interpretation of Intermediate Logics

One of the most remarkable discoveries in the history of logic is that formal proofs can be seen as, and actually are, certified computer programs. Each logical inference corresponds to a natural construct of a functional programming language. This result was first discovered for constructive proofs and then extended to classical ones -- those that may use ineffective principles such as the excluded middle. This correspondence between proofs and programs is known as Curry-Howard isomorphism; it allows logic to become a powerful, bug-free programming language. Nowadays we know how to computationally interpret several expressive logical and mathematical systems, but unfortunately not all of those that matter to us and not as efficiently as possible. In this project we aim to fill an important gap in the theory of the computational interpretation of proofs. Namely, intermediate logics -- logics stronger than intuitionistic logic but weaker than classical -- still do not posses analytic natural deduction systems and Curry-Howard correspondences, but for rare exceptions. They have however a great computational potential. In fact, many intermediate logics include non-constructive axioms, but they have special constructive properties and are more similar to intuitionistic logic than to classical. Moreover, they can model programming mechanisms such as parallelism and message passing between concurrent processes. Since many intermediate logics can be formalized by Avron`s hypersequent calculus, also a full theory of Curry-Howard correspondence can be developed.

The goal of this project was to advance our understanding of parallel computation by means of logic. Parallel programs allow to make several different computations at the same time, and thus solve computational problems faster and more efficiently than sequential programs. Unfortunately, parallel programming is prone to error and there are very few methods that can be used to prove correctness of parallel programs. In this project we used logic as a tool to design and reason about parallel functional programs. We discovered in particular that multiplicative linear logic can be used as a type system for a new, simple, yet expressive parallel extension of simply typed lambda calculus, which is the basis of all functional programming languages. All programs that one can type are correct by construction, that is, they terminate, they don't have deadlocks, they give a result, and always give the same result independently from how they are evaluated. Other results of this project show that intermediate logics, that is, logics that encode constructive reasoning but are contained in classical logical reasoning, can act as type systems for expressive functional programming languages. Namely, one can start from a communication topology that programs should employ for exchanging messages, and automatically obtain a logic that types only processes that communicate according to the topology. This allows complex communication mechanisms, whose correctness and termination is guaranteed by the type system itself.