Structures and Deduction 2009
Bordeaux
July 20 - 24, 2009
Presentation
The topic of this workshop is the application of algebraic, geometric,
and combinatorial methods in proof theory. In recent years many
researchers have proposed approaches to understand and reduce
"syntactic bureaucracy" in the presentation of proofs. Examples are
proof nets, atomic flows, new deductive systems based on deep
inference, and new algebraic semantics for proofs. These efforts have
also led to new methods of proof normalisation and new results in
proof complexity.
The workshop is relevant to a wide range of people. The list of topics
includes among others: algebraic semantics of proofs, game semantics,
proof nets, deep inference, tableaux systems, category theory,
deduction modulo, cut elimination, complexity theory, etc.
The goal of the workshop is twofold: first, to bring together
researchers from various fields who share the interest of
understanding and dealing with structural properties of proofs and
second, to provide an opportunity for PhD students and researchers to
present and discuss their work with colleagues who work in the broad
subject areas that are represented at ESSLLI.
The workshop is intended to be a sequel of the ICALP-workshop SD05 in Lisbon 2005.
Workshop Format
The workshop is part of ESSLLI
2009 in Bordeaux and is open to all ESSLLI participants. It will
consist of five 90-minute sessions held over five consecutive days in
the first week of ESSLLI. There will be 2 or 3 slots for paper
presentation and discussion per session. On the first day the
workshop organizers will give an introduction to the topic.
Invited Speaker
Submission
Contributions can be regular papers, but also work in progress,
programmatic/position papers or tutorials. Submissions should be
formatted with the LNCS LaTeX style, and should take between two and
fifteen pages, to allow the committee to assess their merits with
reasonable effort. This limit can be relaxed for the versions that
will be presented at the workshop, depending on the total bulk of the
accepted contributions.
Please use the SD'09 submission
page http://www.easychair.org/conferences/?conf=sd09,
handled by the EasyChair conference system, to submit papers.
The accepted papers will appear in the workshop proceedings published
by ESSLLI. One author for each accepted paper must attend the
workshop in order to present the paper.
Important Dates
-
Deadline for submissions: March 8, 2009 (extended)
-
Notification of acceptance: April 15, 2009
-
Deadline for final versions: May 11, 2009
-
Workshop dates: July 20 - 24, 2009
Programme Committee
Programme
Invited Lecture
-
François
Lamarche
Title: An interesting link between type theory and topology
Abstract:
Henri Poincaré invented both homology and homotopy theory around
1899. The spaces he used for homotopy were pieces of
R^n glued together; the general concept of topological
spaces had not been invented yet. He could not do the same for
homology, so he resorted to simple combinatorial objects to define the
necessary spaces, which he called simplicial complexes, and where
computations were easy anyway. It is only in the forties that
Eilenberg showed how do define homology directly on topological
spaces, and in the early fifties that combinatorial objects were
found---that we now call simplicial sets, and that are also due to
Eilenberg and his students---which are sufficiently powerful to enable
direct definitions and quite a few computations in homotopy.
The most fundamental concept of homotopy is the notion of path between
two points in a space. For several years it has been tempting to give a
logical meaning to this notion of path, namely as "a constructive
proof that two points are equal". One way to formalize this intuitive
notion would be to interpret the Martin-Löf type-theoretical equality
predicate in a suitable category of spaces. The first positive results
in this direction have been given by Michael Warren, working under the
supervision of Steve Awodey. They are quite technical and depend very
much on modern abstract homotopy theory à la Quillen.
I will present a very concrete model, which I also think is the simplest
that
has been discovered so far. It is based on a well-known specialization of
simplicial set, for which I will define a concrete path object which doubles
as an identity type, along with a suitable notion of dependent type.
I will try keep things as elementary as possible.
(Joint work with Robert Hein)
Contributed Talks
-
Stepan Kuznetsov
Title: On the Lambek calculus with one division and one primitive type
Abstract:
The following theorem is proved: a formal language without the empty
word is context-free if and only if it is generated by some
L(\;p_1)-grammar, where L(\;p_1) is the Lambek calculus with one
division and one primitive type. To do that, we use a substitution of
types which reduces derivability in L(\) to derivability in L(\;p_1).
-
Bruno Woltzenlogel Paleo, Stefan Hetzl, Alexander Leitsch, Daniel
Weller and Tomer Libal
Title: Resolution Refinements for Cut-Elimination based on Reductive Methods
Abstract:
Traditional reductive cut-elimination and CERES seem to be
methods of entirely dierent nature and hence hard to compare. This short
paper describes ongoing research that aims at comparing and possibly
combining them in ways that retain that best features of each method.
-
Kai Brünnler and
Richard McKinley
Title: An Algorithmic Interpretation of a Deep Inference System
Abstract:
We set out to find something that corresponds to deep inference in
the same way that the lambda-calculus corresponds to natural
deduction. Starting from natural deduction for the
conjunction-implication fragment of intuitionistic logic we design a
corresponding deep inference system together with reduction rules on
proofs that allow a fine-grained simulation of beta-reduction.
-
Vincent Aravantinos, Ricardo Caferra and Nicolas Peltier
Title: A DPLL Proof Procedure for Propositional Iterated Schemata
Abstract:
We investigate \emph{iterated schemata} whose syntax integrates arithmetic parameters,
indexed propositional variables (e.g. $P_i$),
and iterated conjunctions/disjunctions (e.g. $\bigwedge_{i=1}^n P_i$, where $n$ is a \emph{parameter}).
Using this formalism gives us some extra information about the structure of the problem,
which can be used in order to prove such a schema \emph{for all values of the parameters}.
The structure of the formula is used as a guide for the structure of the proof.
We define a Davis-Putnam-Logemann-Loveland based procedure for iterated schemata
that we show to be sound and complete (w.r.t. satisfiability).
Though unrestricted schemata are incomplete (w.r.t. provability)
we show, by extending our procedure, that cycles can be detected in the proof tree,
thus allowing to prove some schemata that are neither provable nor refutable in the initial calculus.
An example shows how this method allows to tackle non-trivial problems.
We give evidence that our procedure is a useful tool for
identifying complete classes of schemata.
-
Nicolas Guenot
Title: Concurrency and Permutability in the Sequent Calculus
Abstract:
In proof theory, the sequent calculus has been the most widely used
logical formalism since its inception by Gentzen. However, it uses a
syntax involving a lot of bureaucracy, thus detaining similar proofs
from being written as a unique object. Indeed, different rule
instances in a proof can be permuted, if the order of the
corresponding inference steps does not matter. What we present here is
a work in progress, aiming at a general framework for studying
permutability properties of inference rule instances. To achieve this,
we introduce the permutability graph notion, which provides a unified
syntax for equivalent proofs up to permutations. This could also be
used to prove completeness for proof transformations, especially when
it is based on permutations of inference rule instances.
-
Antoine ElKhoury, Serguei Soloviev, Laurent Mehats and Mark
Spivakovsky
Title: Categorical Semantics and Non-Free Categories
Abstract:
We present several cases where the study of non-free categories and corresponding
categorical semantics on derivations can be interesting and useful to proof-theorists, and where proof-theoretical methods can be successfully used to study
non-free categories. In particular, we consider: 1) equivalences on derivations
generated by interpretations in non-free categories; 2) the triple-dual conjecture and the problem of full coherence in closed categories; 3) varieties of closed
categories with structure (in the sense of universal algebra) - this section contains main new results; 4) the problem of dependency of diagrams; 5) arbitrary
natural transformations and proof-theoretical methods in their study.
-
Willem Heijltjes
Title: Investigations into Forest Proofs
Abstract:
The present document is a brief summary of an ongoing research
programme into forest proofs for first-order classical logic, inspired
by Herbrand's theorem and backtracking games. First described by
Miller in a cut-free setting, this is generalised by adding a notion
of cut. The main result is a cut-elimination theorem.
-
Richard McKinley
Title: The alpha-epsilon calculus
Abstract:
This paper is a brief introduction to the alpha-epsilson calculus --- a
calculus of communication and duplication inspired by the structure of
the classical quantifiers. We will summarize the results of two
recently submitted papers on connections between extensions of the
calculus, sequent systems/proof nets for classical logic, and
Herbrand's theorem.
-
Marco Gaboardi, Luca Roversi and Luca Vercelli
Title: Do Light Logics allow a unified view of Stratification and Boundedness?
Abstract:
This few pages are meant to illustrate an ongoing work whose
goal is to find fine-grained logical principles, in the tradition of structural
proof-theory, on which we can base the definition of a deductive system
that contains both Light Affine Logic and Soft Linear
Logic.
-
Nelson Martins-Ferreira
Title: Naturality and coherence in categories with a 2-cell structure
Abstract:
In his '63 paper on "Natural Associativity and Commutativity", MacLane proved a coherence theorem for natural isomorphisms in a monoidal category, which is easily extended to Bicategories as well. However, if considering a further generalization, from Bicategories to pseudo categories [1], we are faced with the problem of coherence for unnatural isomorphisms. Homotopies between abelian chain complexes are an important example of this situation.
This note is the starting point of such a program where we simply identify the problem and provide some tools that are expected to be useful in the future to find a solution.
[1] N. Martins-Ferreira, "Pseudocategories",JHRS, Vol.1(1),2006, 47-78
-
François
Lamarche and Novak Novakovic
Title: Two Denotational Interpretation of Classical Logic
Abstract:
In this paper we present and compare two interpretations of
classical logic proofs in a category of posets and relations, and
relate their behavior to proof nets, extracting meaningful
invariants of proofs. We show that at least one of these
interpretation cannot have anything to do with the Curry-Howard
correspondence.
Proceedings
The proceedings of the workshop
are available as pdf-file.
Local Arrangements
All workshop participants including the presenters will be required to
register for ESSLLI'09. The
registration fee for authors presenting a paper will correspond to the
early student/workshop speaker registration fee. Moreover, a number of
additional fee waiver grants will be made available by the ESSLLI
local organizing committee on a competitive basis and workshop
participants are eligible to apply for those. There will be no
reimbursement for travel costs and accommodation. Workshop speakers
who have difficulty in finding funding should contact the local
organizing committee to ask for the possibilities for a grant.
See also the ESSLLI'09 webpage.
Social Event
Wine tasting.
When: Friday, July 24, 2009, 14:30.
Where: Château Pape Clément, 216, Avenue Docteur Nancel Pennard (PESSAC).
Directions how to get there.
Organization