Workshop on Proof Theory and Computation
Dresden University of Technology
June 3-14, 2002

Call for Participation

We offer the following talks and courses of five lectures each, aimed at researchers and graduate students with some background in proof theory. The focus of the workshop is on proof theory and computation: we aim at a small, informal event where people have plenty of time to exchange ideas.

Participation in the workshop is free of charge, but limited to a maximum of 25 persons. We provide assistance in finding an accommodation in Dresden, at prices starting from 18 EUR/day. Registration is requested, please send an email to wpt@inf.tu-dresden.de, making sure you include a very brief bio (5-10 lines) stating your experience, interests, etc. We will adopt a selection procedure in case of excessive demand.

This is the list of courses:

Week 1: June 3-7, 2002

Week 2: June 10-14, 2002

Dresden, on the river Elbe, is one of the most important art cities of Germany. You can find world-class museums and wonderful architecture and surroundings. We will organize trips and social events.

Abstracts of Courses

SPECIFYING AND REASONING ABOUT PROGRAMS IN PROOF SEARCH
Dale Miller (Penn State, USA)

Since the proof search paradigm makes use of logical connectives to form (logic) programs, recent work on introducing new logical connectives (such as via linear logic) or exploiting higher-type quantifiers immediately provides us with new programs. These talks shall focus on understanding the expressive power of some of these new logical connectives within logic programs. A running example will involve specifying and reasoning about security protocols.

FORMAL METHODS FOR SECURITY PROTOCOLS
Catuscia Palamidessi (Penn State, USA)

This course will provide an introduction to security protocols and to some of the formal approaches to the specification and verification of their properties. The lectures will cover the basic concepts and principles of security, like symmetric and asymmetric cryptography, and properties such as secrecy, authentication, integrity, anonymity, etc. Then they will focus on formal methods for modelling and reasoning about security protocols, and particularly on techniques deriving from the field of concurrency theory (CSP/FDR, spi-calculus).

Course material

HARMONIC TYPE THEORY
Charles Stewart (TU Berlin)

Despite all the progress made in semantics of programming languages, it is still a scary place for the beginner. By applying insights from proof theory and the philosophy of language, the theory of harmony in logic and type theory hopes to provide a more natural approach than either denotational or operational approaches.

ALGEBRAIC THEORY OF CIRCUITS
Yves Lafont (Université de la Méditerranée, Marseille)

Boolean circuits with several outputs are a model of classical computation. They can be obtained from a finite set of structural and logical gates using parallel and sequential composition. There is also a notion of equivalence of boolean circuits which can be derived from a finite set of relations. We are looking for presentations by generators and relations corresponding to reversible and quantum computation. Up to now, we only achieved a little part of this ambitious program: linear reversible computation. For that purpose, we introduce a notion of canonical form which is also a strategy for solving linear systems. There are deep motivations for developing such a theory.

Handout

OPERADS AND THE GEOMETRY OF COMPUTATION
François Lamarche (Loria & INRIA-Lorraine, Nancy)

The course will start with the elements of Joyal's theory of structure species, which are a very powerful tool for defining data structures and producing generating series for them. Then the concept of operad is introduced by the means of the language of species. Operads are an algebraic structure that enables one to give a geometric/algebraic formulation of many aspects of rewriting, whether it is term or graph rewriting. One example which we will cover is a general theory of correctness criteria for proof nets in linear logic.

THE CALCULUS OF STRUCTURES
Alessio Guglielmi (TU Dresden)

Structures are expressions intermediate between sequents and formulae; the calculus of structures is a formalism for defining logical systems. Like the sequent calculus, it allows for notions like the subformula property and cut elimination. The calculus of structures is in fact a generalization of the sequent calculus, but it can be used to disclose properties of logical systems that are not available in the sequent calculus. It has been used to make existing logical systems entirely local and atomic, and to decompose derivations in novel ways. It is also possible to specify very simple logical systems that are not expressible in the sequent calculus. Since the new notions are mainly modularity, locality and atomicity, applications of the calculus of structures fall naturally in the computational field.

Handout

Abstracts of Talks

COMPILING WITH GRAPH TRANSFORMATIONS
Charles Stewart (TU Berlin)

Graph transformations provide a naturally concurrent model of computation. In this talk I shall introduce a low-level graph transformation system, Port Graph Grammars, that provide a suitable basis for the design of an intermediate representation for a compiler, about a high-level calculus, Attributed Graph Transformation Systems, that provide a reasonable framework for the representation of visual languages aimed at the expression of concurrent code, and about the problem of compiling the high-level language into the low-level representation.

A FRAMEWORK FOR SYMBOLIC PREDICATIONAL LANGUAGES
Birgit Elbl (Universität der Bundeswehr München)

In symbolic predicational programming languages, the use of predicates as in logic programming is essential. The notion of predicate is determined by Prolog's computational interpretation, hence not completely covered by considering sets of ground terms. The languages under consideration are declarative or constitute declarative parts of mixed languages, but can also contain Prolog-style or advanced control. As a corresponding model language, FPL (Framework for Predicational Languages) is introduced.

FPL is a typed term calculus whose operational semantics is given by a reduction relation. Turning reductions into rules and extending them by logical rules in a sequent calculus yields an axiomatic semantics. To reflect the role of the logic programming variables adequately, t-algebras and t-domains (term based algebras and domains) are introduced and used in the denotational semantics.

In the talk, the calculus FPL and the main ingredients of its semantics will be presented.

THE NEED FOR REVERSIBLE SYNTAX
François Lamarche (Loria & INRIA-Lorraine, Nancy)

FIXED POINT SEMANTICS FOR LOGIC PROGRAMMING AND NONMONOTONIC REASONING: A UNIFORM APPROACH
Pascal Hitzler (TU Dresden)

Declarative semantics in logic programming and nonmonotonic reasoning are often defined via fixed points of semantic operators. While many relationships between the different semantics known from the literature have been studied, a uniform treatment is still missing.

In the talk, we will provide uniform operator-free characterizations for some of the most important semantics based on monotonic operators, including the Fitting semantics and the well-founded semantics. The characterizations use level mappings and resemble the definition of acceptable programs due to Apt and Pedreschi (1993).

Furthermore, we will also employ level mappings for the study of fixed-point semantics based on nonmonotonic operators. For this purpose, spaces of interpretations are cast into generalized metric spaces such that corresponding fixed-point theorems can be applied. We will discuss this approach in detail for the supported model semantics, which is based on the nonmonotonic immediate consequence operator for programs with negation.

REFLECTING BDDS IN COQ
S. Arun-Kumar (IIT Delhi)
Jointly with Kumar Neeraj Verma, Jean Goubault-Larrecq, Sanjiva Prasad

We describe an implementation and a proof of correctness of binary decision diagrams (BDDs), completely formalized in Coq. This allows us to run BDD-based algorithms inside Coq and paves the way for a smooth integration of symbolic model checking in the Coq proof assistant by using reflection. It also gives us, by Coq's extraction mechanism, certified BDD algorithms implemented in Caml. We have also implemented and proved correct, a garbage collector for our implementation of BDDs inside Coq. Our experiments show that this approach works in practice, and is able to solve both relatively hard propositional problems and actual industrial hardware verification tasks.

Venue

Ratszimmer (room 233)
Computer Science Department
Hans-Grundig-Str. 25
01307 Dresden
Tel.: +49 (351) 463 38340 (Sylvia Epp, secretary)

On Monday, June 10, lectures will take place in room 350.

Every day room 358 will be available for discussions from 16:40 to 20:00.

In the first two weeks of June Dresden is hot and possibly windy; sometimes it rains.

Timetable

The workshop starts at 13:30 on Monday, June 3, with a brief welcome.
Every day lunch will be at 12:15; the workshop ends at 16:30.
Tuesday afternoons: Graduiertenkolleg talk.

Week 1: June 3-7, 2002

MON TUE WED THU FRI
9:30 CS CS CP CP
10:45 b b b b
11:00 DM DM DM DM
13:45 DM CSt CP CP CP
15:00 b b b b b
15:15 CS BEt CS CS

BEt = talk by Birgit Elbl
DM = course by Dale Miller
CP = course by Catuscia Palamidessi
CS = course by Charles Stewart
CSt = talk by Charles Stewart
b = coffee break

Week 2: June 10-14, 2002

MON TUE WED THU FRI
9:30 YL YL YL YL
10:45 b b b b
11:00 FL FL FL FL
13:45 FL* FLt AG AG AKt
15:00 b* b b b b
15:15 AG* AG YL PHt AG

AG = course by Alessio Guglielmi
AKt = talk by S. Arun-Kumar
PHt = talk by Pascal Hitzler
YL = course by Yves Lafont
FL = course by François Lamarche
FLt = talk by François Lamarche
b = coffee break

* On Monday, June 10, lectures will take place in room 350.

Organization

This workshop is organized by the AI Institute at TU Dresden, and sponsored by IQN (Rational mobile agents and systems of agents) and Graduiertenkolleg 334 (Specification of discrete processes and systems of processes by operational models and logics).

Back to the Calculus of Structures

22.10.2002Alessio Guglielmiemail