NEW The program of the workshop is now available.
NEW The electronic proceedings are currently available here; they will be available soon as electronic Technical Report of the Technische Universität Dresden.
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 of proofs game semantics proof nets deductive proof nets |
<—> |
deep inference operads and structads calculus of structures |
<—> |
deduction modulo specification proof search 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.
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 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. We want to make clear that submissions from members of the PC are allowed.
Contributions should be submitted electronically at this site (powered by EasyChair, thanks to Andrei Voronkov).
The volume of proceedings will be available electronically, allowing authors to keep their copyrights. The issue of printed proceedings is still under discussion.
Lisbon, July 16-17, 2005; the workshop is a satellite of the ICALP 2005 conference.
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.
2.7.2005 Paola Bruscoli email