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:

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 Miller

Operational 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 morningCalculus of Structuresmeeting

Thursday 20.11 afternoonProof Netstalks

Friday 21.11 morningDeduction Modulotalks

Friday 21.11 afternoonLogical Frameworkstalk

Modal Logicstalk

Structadstalk

21.11.2003Alessio Guglielmiemail