Campus Event Calendar
Event Entry
What and Who
Proof Nets for Intuitionistic Logic
Matthias Horbach
IMPRS
Talk
AG 1, AG 2, AG 3, AG 4, AG 5, SWS
AG Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Monday, 10 July 2006
08:30
330 Minutes
E1 4
024
Saarbrücken
Abstract
Proof theory is interested mainly in the questions "What is a proof?" and
"When are two proofs equal?". Girard answered these questions in 1986 for
linear logic by developing proof nets. Proof nets constitute a proof system
that abstracts away syntactic bureaucracy (e.g. the order in which subgoals
are proved) and thus gets close to the real essence of proofs.
In this talk, I will turn the focus towards intuitionistic logic, a
fragment of classical logic in which all proofs must be constructive. This
logic is important for example as the theoretical foundation of functional
programming.
I will present a translation of the simply typed lambda-calculus, a
well-examined proof system for intuitionistic logic, into a new kind of
proof nets that are especially suited for intuitionistic logic. I will
analyze the meaning and shape of these nets. Moreover, I will introduce a
strongly normalizing and confluent reduction procedure for the new proof
nets. The result of these explorations is a new notion of the equivalence of
intuitionistic proofs.
"When are two proofs equal?". Girard answered these questions in 1986 for
linear logic by developing proof nets. Proof nets constitute a proof system
that abstracts away syntactic bureaucracy (e.g. the order in which subgoals
are proved) and thus gets close to the real essence of proofs.
In this talk, I will turn the focus towards intuitionistic logic, a
fragment of classical logic in which all proofs must be constructive. This
logic is important for example as the theoretical foundation of functional
programming.
I will present a translation of the simply typed lambda-calculus, a
well-examined proof system for intuitionistic logic, into a new kind of
proof nets that are especially suited for intuitionistic logic. I will
analyze the meaning and shape of these nets. Moreover, I will introduce a
strongly normalizing and confluent reduction procedure for the new proof
nets. The result of these explorations is a new notion of the equivalence of
intuitionistic proofs.
Contact
Kerstin Kathy Meyer-Ross
226
--email hidden
passcode not visible
logged in users only
Jennifer Gerling, 06/30/2006 10:04 -- Created document.