Proposal for a workshop in Lisbon

Hello,

as many of you know, we are about to submit a proposal for a workshop 
to be held in Lisbon, next July, attached to the ICALP conference. 
I'm sending this email to the invited speakers, the PC members and 
the Frogs mailing list. (For those who don't know Frogs, here is a 
description: <http://www.prooftheory.org/frogs>). I'm asking you to 
provide feedback on a call for papers outlining the themes of the 
workshop.

In the past we organised a series of workshops in Dresden, more or 
less about the same topics of the following proposal.
<http://www.computational-logic.org/iccl/events/WPT-2004/>
<http://www.ki.inf.tu-dresden.de/%7eguglielm/WSPT/index.html>
<http://www.cl.inf.tu-dresden.de/compulog/events/workshop.html>

This time we feel that we are ready for a broader participation, and 
we also think this is a good way of terminating a two-year research 
grant we shared between Nancy and Dresden that has been extremely 
fruitful.

So, I'm asking you for comments and suggestions about the call for 
papers, which you find below, and whether you might consider 
submitting a paper to this workshop. It is very important for us to 
have an estimate of the number of participants, so please let us know.

It is very urgent, the proposal and the number of expected 
participants must be sent before Sunday, please answer now. (Sorry 
for the hurry: the idea occurred to Charles only very recently).

Ciao,
-Paola

-------------------------

STRUCTURES AND DEDUCTION
The quest for the essence of proofs

This meeting is about new algebraic and geometric methods in proof 
theory, with the aim of expanding our ability to manipulate proofs, 
eliminate bureaucracy from deductive systems, and ultimately provide: 
1) a satisfying answer to the problem of identity of proofs and 2) 
tools for improving our ability to implement logics.

Stimulated by computer science, proof theory is progressing at fast 
pace. However, it is becoming very technical, and runs the risk of 
splitting into esoteric specialties. The history of science tells us 
that this has happened several times before, and that these 
centrifugal tendencies are very often countered by conceptual 
reunifications, which occur when looking at a field after having 
taken a few steps back.

Some emerging ideas are showing their unifying potential. Deep 
inference's atomization of deductions simplifies and unifies the 
design of deduction systems; it provides unprecedented plasticity to 
proofs and has injected new impetus in the theory of proof nets. New 
proof nets, and new associated semantics, are giving surprising 
insights about the very subtle relationship between categories and 
proofs, for example in the formerly intractable case of classical 
logic. The field of deduction modulo, which turns out to be very much 
in the spirit of deep inference, decreases our dependency on the 
syntactic presentation of functional objects, and brings us closer to 
their intrinsic nature, even from the computational point of view. 
After studying all those trees for years we have the impression of 
finally be looking at the forest.

The core topics are organised along the axis:

  algebraic semantics       deep inference          deduction modulo
  of proofs
                            operads and             specification
  proof nets         <-->   structads        <-->
                                                    proof search
  deductive                 calculus of
  proof nets                structures              implementations

This workshop aims at being a meeting point for all those who are 
interested in decreasing the dependency of logic from low-level 
syntax. The list of topics above is not exhaustive: if you feel you 
can contribute to the discussion along the broad lines outlined 
above, please submit your contribution.

IMPORTANT DATES

submission: 15.4.2005
notification: 22.5.2005
final version: 10.6.2005

INVITED SPEAKERS

Martin Hyland (Cambridge)
Helene or Claude Kirchner (LORIA & INRIA Lorraine, Nancy)
Dale Miller (INRIA Futurs and LIX, Paris)
David Pym (Bath)

PROGRAM COMMITTEE

Roy Dyckhoff (St Andrews)
Rajeev Gore' (NICTA, Canberra)
Francois Lamarche (LORIA & INRIA Lorraine, Nancy)
Luke Ong (Oxford)
Michel Parigot (CNRS, Paris)
Prakash Panangaden (McGill)
Charles Stewart (Dresden)
Thomas Streicher (Darmstadt)

pending:
Paola Bruscoli (Dresden)
Gilles Dowek (LIX & Ecole Polytechnique, Paris)

LOCATION

Lisbon, July 16-17, 2005

ORGANISERS

Paola Bruscoli (Dresden)
Francois Lamarche (LORIA & INRIA Lorraine, Nancy)
Charles Stewart (Dresden)