Computational Structure of Classical Duality
The Curry-Howard correspondence, also known as the proofs-as-programs correspondence, is the observation that logical proofs and computer programs are two ways of presenting the same mathematical objects. This project aims to extend the scope of the correspondence in two important directions: on the logical side, towards capturing classical logic, the logic used in natural and mathematical reasoning, and on the computational side to the idea of a ``process``; a program which interacts with many other programs by passing messages.
Background: In the 1930s, Alonzo Church developed a calculus (the lambda calculus) a language for writing down what we now call computable functions. At the same time Gerhard Gentzen was developing natural deduction; a language for writing down formal proofs. Both these languages were conceived as tools for exploring the foundations of mathematics, with the advent of computer science, representations of computable functions became a more practical concern. Lambda calculus was the inspiration for Lisp, the first functional programming language. Meanwhile, William Alvin Howard discovered a link between logic and functional programming: natural deduction proofs could be seen themselves as terms of the lambda calculus. In other words, a proof is a kind of computation, and a very well-behaved kind at that. This observation, known as the Curry-Howard correspondence, has led and continues to lead to an enormous body of theoretical and practical work in computer science and logic.
Goals of the project: Computer science has developed much since its inception, and we no longer think of computer problems as simply calculating a function, but more as interacting with a complex, varying environment comprised of users and other programs. The lambda calculus is unsuited for representing such programs, and other calculi (called process calculi) are used instead to reason about them. These calculi lack the elegant theoretic underpinning enjoyed by the lambda calculus. On the other hand, natural deduction fails to faithfully represent a fundamental reasoning mode: the ability to recognize that a statement is the same as its double negation. This property of logic is called "Duality". A much better calculus for reasoning under duality, called the sequent calculus, was also developed by Gentzen, but its computational meaning has been difficult to discern.
This project aims to extend the proofs as programs correspondence by representing proofs using duality within a new, theoretically inspired language of processes.
