18.473 Structures and Deduction Workshop

               Humanist Discussion Group, Vol. 18, No. 473.
       Centre for Computing in the Humanities, King's College London
                   www.kcl.ac.uk/humanities/cch/humanist/
                        www.princeton.edu/humanist/
                     Submit to: humanist_at_princeton.edu

         Date: Sat, 08 Jan 2005 10:20:13 +0000
         From: Paola Bruscoli <Paola.Bruscoli_at_Inf.TU-Dresden.DE>
         Subject: Structures and Deduction Workshop CfP - ICALP '05 Satellite

ICALP Workshop-Lisbon July 16-17, 2005

STRUCTURES AND DEDUCTION
The quest for the essence of proofs
<http://www.prooftheory.org/sd05>

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 one is 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 into the theory of proof nets.
New proof nets, and new associated semantics, are giving surprising
insight 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 at last have the
impression of looking at the forest.

The core topics are organised along the axis:

     algebraic semantics deduction
     of proofs deep inference modulo

     game semantics operads and specification
                        <--> structads <-->
     proof nets proof search
                               calculus of
     deductive structures implementations
     proof nets

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.

SUBMISSION, IMPORTANT DATES AND PUBLICATION

Contributions such as work in progress, programmatic/position papers,
tutorials, as well as regular papers are more than welcome. We will
favor the former over regular papers that seem to us to be minor
contributions, although we will definitely not reject major
contributions!

Submissions should be formatted with the LNCS LaTeX style, and should
not exceed 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.

Contributions should be submitted electronically; details will be
provided soon.

submission: 15.4.2005
notification: 22.5.2005
final version: 10.6.2005

The selected papers will be made public on the web for downloads. It
goes without saying that authors will be able to keep their
copyrights.

The issue of printed proceedings is still under discussion.

INVITED SPEAKERS

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

PROGRAM COMMITTEE

Paola Bruscoli (Dresden)
Pietro Di Gianantonio (Udine)
Gilles Dowek (LIX & Ecole Polytechnique, Paris)
Roy Dyckhoff (St Andrews)
Rajeev Gore' (NICTA and ANU, Canberra)
Francois Lamarche (LORIA & INRIA Lorraine, Nancy) -- Chair
Luke Ong (Oxford)
Prakash Panangaden (McGill)
Michel Parigot (CNRS, Paris)
Charles Stewart (Dresden)
Thomas Streicher (Darmstadt)

LOCATION

Lisbon, July 16-17, 2005; the workshop is a satellite of the ICALP
2005 conference.

HOW TO REGISTER

A registration fee for attending the workshop will be paid to the
ICALP Workshop general chair; no fee for participating in the main
conference should be necessary, while participation in both conference
and workshop should entitle to special discounts. Please visit the
ICALP web site for up-to-date, precise information:
<http://icalp05.di.fct.unl.pt>

ORGANISERS

Paola Bruscoli (Dresden)
Francois Lamarche (LORIA & INRIA Lorraine, Nancy) -- Chair
Charles Stewart (Dresden)
Received on Sat Jan 08 2005 - 05:33:16 EST