# Project

Back to overview

## Computational Structure of Classical Duality

 Applicant McKinley Richard 126422 Ambizione Institut für Informatik Universität Bern University of Berne - BE Information Technology 01.03.2010 - 28.02.2013 434'641.00 Show all

### All Disciplines (2)

Discipline
 Information Technology
 Mathematics

### Keywords (5)

Proof theory; Logic; Computer Science; Category Theory; Process Algebra

### Lay Summary (English)

Lay summary
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 practicle 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 recognise 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.
 Direct link to Lay Summary Last update: 21.02.2013

### Responsible applicant and co-applicants

Name Institute
 McKinley Richard University Institute for Diagnostic and Interventional Neuroradiology (SCAN) Inselspital

### Employees

Name Institute
 McKinley Richard University Institute for Diagnostic and Interventional Neuroradiology (SCAN) Inselspital

### Publications

Publication
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.

### Scientific events

#### Active participation

Title Type of contribution Title of article or contribution Date Place Persons involved
 Workshop on Non-classical logics 25.11.2011 Wien
 Topology, Algebra, Categories and Logic 26.07.2011 Marseilles

#### Self-organised

Title Date Place
 Gentzen Systems and Beyond 04.07.2011 Bern

### Associated projects

Number Title Start Funding scheme
 145747 Computational structure of higher-order sequent calculi 01.03.2013 Ambizione

### Abstract

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.
-