Proof theory; Logic; Computer Science; Category Theory; Process Algebra
McKinley Richard (2013), Canonical Proof Nets for Classical Logic, in Annals of Pure and Applied Mathematics
, 164(6), 702-732.
McKinley Richard (2013), Proof Nets for Herbrand's Theorem, in ACM Transactions on Computational Logic
, 14(1), 5.
McKinley Richard (2010), Expansion nets: Proof nets for for propositional classical logic, in Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR
, Yogyakarta, IndonesiaSpringer, BERLIN/HEIDELBERG.
The Curry-Howard correspondence, also known as the proofs-as-programs correspondence, is the observation that proofs and programs are two ways of presenting the same mathematical objects. The most fully developed correspondence of this kind is between intuitionistic logic (roughly, logic without the law of excluded middle) and typed lambda calculus, where proofs in natural deduction correspond to prototypic functional programs. A proof deriving a formula A from a set of assumptions G can be viewed as a program with parameters G, deriving data of type A. In this setting, computation is normalization: a process of removing “detours” from a proof which simpli?es its logical structure. The correspondence applies for propositional, ?rst-order and higher-order logics/type theories, and has been the source of numerous useful insights in both proof theory and programming language design. In particular, the uni?ed semantical theory of proofs/programms in this setting (interpretation in a cartesian-closed category) gives a way to say when two proofs (or two programs) are essentially the same.This project will make contributions to the proofs-as-programs correspondence for classical logic, which is the underlying logic of mathematical practice, and also underpins mant important applications in computer science (speci?cation, veri?cation, circuit design, etc). There have been many attempts to give such a correspondence, but (unlike for intuitionistic logic) there is no general theory of correspondence. This is perhaps unsurprising, as the nature of classical proof itself is poorly understood.The project I propose has two goals:1: To increase our understanding of proving as dialogue (a proof is a strategy for playing a game) by developing formal calculi of strategies and by relating existing notions of proof to game notions of proof. 2: to develop, via the above game theoretic understanding, a theory of classical proofs as processes.