**Workshop on Structural Proof Theory
Technische Universität Dresden
November 19-21, 2003**

This meeting is dedicated to structural proof theory and related matters. The meeting will mostly take place on November 20 and 21. November 19 is holiday here, but some of us meet nonetheless and the workshop room is available.

**Participants**

From Bern:

From INRIA-Lorraine, Nancy:

From Paris VII:

- Jean-Baptiste Joinet
- Michel Parigot

From Penn State:

Locals:

**Talks**

Induction as Deduction Modulo

Eric Deplagne (INRIA-Lorraine)

Completeness of Weak-distributivity W.R.T. Multiplicative Proof-nets

Jean-Baptiste Joinet (Paris VII)

From Deduction to Computation in the Calculus of Structures via Term Rewriting

Ozan Kahramanogullari (TU Dresden)

From Structads to the Calculus of Structures: The Story So Far

François Lamarche (INRIA-Lorraine)

A Proof Theoretical Method for the Generation Problem in Type Logical Grammars

Sylvain Pogodalla (INRIA-Lorraine)In this talk, I present the principles of type logical grammars. I state the problems of parsing and generation in the usual framework of logic for syntax (linear logic, Lambek calculus), and typed lambda-calculus for semantics. Generation is then seen as a lambda-term matching problem. Then I restate the problem of generation in the logical framework of proofnets and show how the execution formula of the geometry of interaction arises. It suggests an algebraic solution to that problem and allows a characterization of the lexical items that make the solution computation quadratic. Then I conclude on other problems of NLP to which this method could apply.

What is the problem with the proof theory of modal logic?

Charles Stewart (TU Dresden)

Multiplicative Additive Proof Nets

Lutz Straßburger (INRIA-Lorraine)

A Logical Framework for Reasoning with Names

Alwen Tiu (Penn State), joint work with Dale MillerOperational semantics of most modern calculi often involves the use of names, e.g., as reference to locations, place-holders for values (in imperative languages), nonces in security protocol, etc. There are some common features in the use of names in those calculi, notably, the notions of binding, scoping and "freshness" of names. I will present a new logical system, which is a conservative extension of intuitionistic logic, and show that these notions can be given a logical interpretation via the use of quantifiers. One novelty of the logic is the addition of a new quantifier, nabla, which is, roughly speaking, the "intensional" part of the universal quantifier. As a running example, I'll show an encoding of late pi-calculus. We'll see that the notion of strong equivalence (up to distinction of names) as defined by Milner can be captured properly by the alternation of universal and nabla quantifiers.

**Venue**

Room 357

Computer Science Department

Hans-Grundig-Str. 25

01307 Dresden

Tel.: +49 (351) 463 38340 (Sylvia Epp, secretary)

See here how to reach us.

**Timetable**

Thursday 20.11 morning**Calculus of Structures**meeting

- 10:00 Kai Brünnler and Alessio Guglielmi

Cut elimination in classical logic (several old and new results, discussion)

Thursday 20.11 afternoon**Proof Nets**talks

- 13:30 Sylvain Pogodalla
- 14:45 Jean-Baptiste Joinet
- 16:00 Lutz Straßburger

Friday 21.11 morning**Deduction Modulo**talks

- 10:00 Eric Deplagne
- 11:15 Ozan Kahramanogullari

Friday 21.11 afternoon**Logical Frameworks**talk

- 14:00 Alwen Tiu

**Modal Logics**talk

- 15:00 Charles Stewart

**Structads**talk

- 16:00 François Lamarche