## Contact

Swiss National Science Foundation (SNSF)

Wildhainweg 3P.O. Box

CH-3001 Bern

Phone +41 31 308 22 22

Applicant | McKinley Richard |
---|---|

Number | 126422 |

Funding scheme | Ambizione |

Research institution | Institut für Informatik Universität Bern |

Institution of higher education | University of Berne - BE |

Main discipline | Information Technology |

Start/End | 01.03.2010 - 28.02.2013 |

Approved amount | 434'641.00 |

Discipline |
---|

Information Technology |

Mathematics |

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

Lead |
---|

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 |

Name | Institute |
---|

Name | Institute |
---|

Publication |
---|

Canonical Proof Nets for Classical Logic |

Proof Nets for Herbrand's Theorem |

Expansion nets: Proof nets for for propositional classical logic |

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 |

Title | Date | Place |
---|

Gentzen Systems and Beyond | 04.07.2011 | Bern |

Number | Title | Start | Funding scheme |
---|

145747 | Computational structure of higher-order sequent calculi | 01.03.2013 | Ambizione |

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.

Swiss National Science Foundation (SNSF)

Wildhainweg 3P.O. Box

CH-3001 Bern

Phone +41 31 308 22 22

Enter and manage your applications

Enter your e-mail address to receive the SNSF Newsletter regularly

© SNSF 2018