This workshop is devoted to proof theory, from the design of deduction systems for various logics (classical, intuitionistic, modal,...) via computational interpretations of proofs through cut-elimination to proof-search and applications in logic programming.
There will be 4 invited talks and the rest of the programme will consist of contributed talks and discussions.
The workshop is open to everyone interested. All proposals of contributed talks are welcome, including work in progress and discussion of open problems.
If you intend to give a talk or simply participate, please let us know by sending an email to stefan.hetzl[at]pps.jussieu.fr.
This workshop is sponsored by the Kurt Gödel Society.| 10.00 - 11.00 | Daniel Leivant : Ramified second order logic and computational complexity | |
| 11.00 - 11.30 | Coffee | |
| 11.30 - 12.00 | Nicolas Guenot: A computational account of cut-elimination in nested sequents for intuitionistic logic | |
| 12.00 - 12.30 | Anne-Laure Poupon: A game for MALL with focus | |
| 12.30 - 14.00 | Lunch | |
| 14.00 - 15.00 | Konstantin Korovin: Modular instantiation-based automated reasoning | |
| 15.00 - 15.30 | Matthias Baaz: Resolution based proof procedures for First Order Goedel logics | |
| 15.30 - 16.00 | Coffee | |
| 16.00 - 17.00 | Daniel Weller: Proof search in cut-elimination | |
| 17.00 - 17.30 | Lutz Straßburger: Decidability of Pseudo-Transitive Modal Logics | |
| 17.30 - 18.00 | David Baelde: Combining fixed-point and recursive definitions |
There will be a dinner on Monday evening at 20.00 in the restaurant
Les Papilles en Folie, 2 rue Duchefdelaville, 75013 Paris,
map
to which all participants are invited.
| 10.00 - 11.00 | Olivier Laurent: Type isomorphisms for classical logic | |
| 11.00 - 11.30 | Coffee | |
| 11.30 - 12.00 | Noam Zeilberger: A few observations on substructural logic and computational effects | |
| 12.00 - 12.30 | Marc Lasson: Realizability and Parametricity in Pure Type systems | |
| 12.30 - 13.00 | Stéphane Gimenez: Using structures to fix (or improve) several systems of nets derived from Linear Logic |
Lunch will be provided for all participants on both days.
David Baelde: Combining fixed-point and recursive definitions
Abstract:
Fixed point and recursive definitions are powerful
specification tools used in many formal developments. Those two
concepts, although similar, should not be confused. We'll see that a
careful distinction is needed to obtain a proper proof-theoretical
support for the two. On our course to establish cut-elimination for a
logic supporting both kinds of definitions, we'll encounter deduction
modulo, which turns out to be complementary to definitions in the
style of Schroeder-Heister. When combining the two traditions, the
crucial problem lies in the treatment of equality. This is work in
progress with Gopalan Nadathur.
Stéphane Gimenez: Using structures to fix (or improve) several systems of
nets derived from Linear Logic
Abstract:
I will present three systems based on interaction nets that cannot be
"typed" satisfactorily with Sequent Calculus, but that could be typed
using a (slightly modified) Calculus of Structures. This is work in
progress.
Nicolas Guenot: A computational account of cut-elimination in nested sequents for intuitionistic logic
Abstract:
I will present a nested sequent calculus, where sequents can appear inside
other sequents, for (implication-only) propositional intuitionistic logic,
and discuss a cut elimination procedure based on rule permutations. Then, I
will show how to use this system as a type system for a lambda-calculus with
explicit substitutions, and explain how cut elimination on typing derivations
can be reflected as reduction on the lambda-terms. In particular, I will
discuss the decompositions allowed by the deep inference methodology and
present the problems encountered when trying to build a precise correspondence
between reductions and cut-elimination steps.
Konstantin Korovin: Modular instantiation-based automated reasoning
Abstract:
Automated reasoning has a number of applications
ranging from verification of software and hardware
to reasoning with large ontologies and knowledge-bases.
Instantiation-based automated reasoning
aims at utilising industrial-strength SAT and SMT technologies
in the more general context of first-order logic.
The basic idea behind instantiation-based reasoning is
to combine smart generation of instances with satisfiability
checking of ground formulae.
There are a number of challenges arising in this area:
theoretical issues such completeness,
integration of theories and decidable fragments;
and issues related to efficient implementation: inference strategies,
indexing and redundancy elimination.
In this talk I will overview the recent advances
in instantiation-based reasoning, focusing on a modular approach which
allows us to use off-the-shelf SAT and SMT solvers for ground formulae
as part of general first-order reasoning.
Marc Lasson: Realizability and Parametricity in Pure Type systems
Abstract:
We describe a systematic method to build a logic from any
programming language described as a Pure Type System (PTS). The
formulas of this logic express properties about programs. We define a
parametricity theory about programs and a realizability theory for the
logic. The logic is expressive enough to internalize both theories. Thanks
to the PTS setting, we abstract most idiosyncrasies specific to particular
type theories. This confers generality to the results, and reveals
parallels between parametricity and realizability.
Olivier Laurent: Type isomorphisms for classical logic
Abstract:
In a typed programming language, the question of type isomorphisms
consist in understanding when two types can be considered to represent
the same thing. Once this is properly formalised, the problem becomes
to find an equational theory characterising these isomorphisms.
Through the Curry-Howard-Lambek correspondence, this question can also
be stated for a given logic or for some categorical structure.
In this way the type isomorphism problems for:
- the simply typed lambda-calculus with arrow, product and unit types,
- intuitionistic logic with implication, conjunction and true,
- cartesian closed categories
are the same.
We will survey some of the results around type isomorphisms for
intuitionistic and linear logics, and then turn to the case of
classical logic (with important distinctions between a call-by-name
and a call-by-value setting).
Daniel Leivant: Ramified second order logic and computational complexity
Abstract:
Ramification in logic goes back to Whitehead and Russell's Type Theory
over a century ago, and was formalized by Schutte in 1960.
We make the case that ramified second order logic is an attractive master
formalism for descriptive and deductive aspects of computational complexity.
Our main technical observations have to do with ramified recurrence and
corecurrence. Ramification of recurrence has been used for
some time to provide implicit characterizations to computational
complexity classes, in particular polynomial time.
We show that ramification of recurrence can be construed as syntactic
sugar for ramification in second order logic.
We give a natural characterization of PTime by provability in
ramified second-order logic, and observe a dual characterization for
streams.
Anne-Laure Poupon: A game for MALL with focus
Abstract:
Usually, when trying to prove whether a formula F is true or not, the
only way is to assume it must be true, and look for a proof. If there
isn't any, maybe we have a counterexample, but if we want to find a
proof for the negation of F, we need to start the whole proof search
from the beginning.
Here we propose a game semantics that allows us to simultaneously
search for a proof of F and for a proof of its negation. This is still
work in progress, the aim is to obtain such a semantics for linear
logic. To do it, we have started with LKF+ (classical logic with focus
with only positive connectives), and then extended the games to LKF,
and then to MALL with focus. The major difference with usual games is
that here the Player works to prove F, and the Opponent, instead of
just trying to reach a counterexample to F, works to prove the
negation of F.
This can be useful for open problems, for which we cannot make any
relevant conjectures, and helps us understand how a failure in proof
search can still give us some information to prove the opposite.
Lutz Straßburger: Decidability of Pseudo-Transitive Modal Logics
Abstract:
We call a modal logic "pseudo-transitive" if it obeys the axiom
"box box A implies box box box A". The question whether the modal
logic K extended with this axiom is decidable, is a known open
problem. In this paper, I will present a cut-free deductive system
which is sound and complete for that logic, and which is suitable
for proof search. In fact, the system induces a terminating proof
search procedure, which entails decidability of the logic.
Independently from cut elimination, I will also give a
semantic proof of the finite model property.
Daniel Weller: Proof search in cut-elimination
Abstract:
Given a proof P with cuts of a theorem T, there are different ways to
obtain a cut-free proof of T: the usual way is to transform P by applying
certain syntactic reduction rules in a terminating way. Another
possibility is to apply a cut-free completeness argument to T: that is, to
construct a cut-free proof of T given the fact that T is valid. It may
appear that this second possibility is less suited, since the assumption
"T is valid" contains less computational information than P, and the
cut-free proof is usually found by search. In this talk, we discuss how to
strengthen this approach by searching for a cut-free proof of T' instead
of T, where T' is a valid formula extracted from P which contains more
information from P than T. We will recall the CERES method, which
informally is an instance of this idea for classical logic. Finally, we
will present work-in-progress on applying this idea to intuitionistic
logic.
Noam Zeilberger: A few observations on substructural logic and computational effects
Abstract:
I will discuss work-in-progress motivated by the desire to
refashion linear logic as a language of computational effects. For
this end, it is natural to start from *non-commutative* linear logic,
but I will also take the opportunity to revisit basic questions about
the semantics of proofs, and in particular motivate the
non-commutative setting by a sort of abstract adjunction between types
and contexts.
| Last Change: 2011-02-27, Stefan Hetzl |
|