Summer School and Workshop on
Proof Theory, Computation and Complexity
Technische Universität Dresden
June 23-July 4, 2003
Call for Participation
We plan the following courses and workshop for graduate students and researchers. Like for last year’s events on `Proof Theory and Computation´ (Dresden) and `Proof, Computation, Complexity´ (Tübingen), we aim at a meeting where people have plenty of time to exchange ideas. The summer school consists of nine advanced courses; the workshop is integral part of the school and takes place in the last two days.
For attending courses, we ask for a fee of 100 EUR (to be paid in cash at the school). Registration is requested before May 25, 2003; please send an email to PTEvent@Janeway.Inf.TU-Dresden.DE, making sure you include a very brief bio (5-10 lines) stating your experience, interests, home page, etc. We select applicants in case of excessive demand. A limited number of grants covering all expenses is available. Applications for grants must include an estimate for travel costs and they should be sent together with the registration. We provide assistance in finding an accommodation in Dresden.
Week 1, June 23-27: courses on
Week 2
June 30-July 2: courses on
July 3-4: workshop
Talks by Kai Brünnler, Birgit Elbl, Pascal Hitzler, Reinhard Kahle, Vladimir Komendantsky, Lars Kristiansen, Karl-Heinz Niggl, Isabel Oitavem, Monika Seisenberger, Charles Stewart, Lutz Straßburger, Alwen Tiu, Heinrich Wansing and Henning Wunderlich.
For more details, please consult the workshop web page.
Denotational Semantics of Lambda Calculi
Achim Jung (Birmingham, UK) – 5 lecturesThe lectures intend to give an introduction into the problems posed by trying to construct a mathematical model for higher-order computation. The term "higher-order" here refers to various lambda calculi which embody crucial features of working with functions at higher types.
After introducing the simply typed lambda calculus, it is planned to present Friedman's completeness theorem for infinite Henkin models. Friedman's proof is one of the first applications of the idea of "logical relation", later extended and developed by Plotkin and Statman. We then move on to a typed calculus extended with a notion of recursion, commonly known as the language PCF. Modelling recursion requires us to extend semantic spaces with more structure and so we will have to introduce some of the ideas behind Domain Theory. This part of the course concludes with a proof of "adequacy" (which is correctness and completeness at ground types). In the last part we will look at modelling the untyped lambda calculus. Again, a major technical difficulty arises and we will overcome it by constructing inverse limits of domains.
The course will not strictly assume knowledge of the lambda calculus but participants who are already familiar with its syntactic theory will gain most from it.
Proof Theory with Deep Inference
Alessio Guglielmi (Dresden, Germany) – 3 lecturesProof theory has been developed for formalisms that adopt shallow inference, like the sequent calculus, natural deduction and proof nets. In these calculi, inference is based on the external shape of formulae: rules have no visibility of formulae beyond a bounded neighborhood of their root. It is actually possible to adopt deep inference, where deduction can be performed inside formulae at any depth. This is an old idea of Schütte that was never brought to its ultimate consequences: his treatment is concise but not broader than what is possible without deep inference.
As we discovered recently, deep inference allows for a radically new, simple and elegant proof theory, when coupled with a notion of premise-conclusion symmetry. A new range of possibilities is open, with direct impact on computer science. We can in fact design deductive systems for important logics, like classical, linear and modal logics, whose rules are all local and atomic, including cut, contraction, promotion, additive context management, etc. Moreover, several modularity properties hold that are provably impossible for shallow calculi. We can study logics arising from process algebras for which no presentation in shallow calculi exists. We can also study new, meaningful notions of normalisation.
Slides (web site on the Calculus of Structures)
Semantics and Cut-elimination for Church's (Intuitionistic) Theory of Types, with Applications to Higher-order Logic Programming
Jim Lipton (Wesleyan, USA) – 3 lectures1. Review of cut elimination and completeness for First Order Logic. Tableaux. Intuitionistic Logic. Kripke models. Kripke lambda models.
2. Church's Theory of Types (classical and intuitionistic). Lambda-Prolog.
3. Completeness and cut-elimination for the Intuitionistic Theory of Types.
Proof Analysis
Sara Negri (University of Helsinki and Academy of Finland) – 4 lecturesThe course gives a concise introduction to the central methods and results of structural proof theory. Special emphasis is given to the design of sequent calculi supporting proof-search and to the extension of logical calculi with mathematical rules. Expected background is an introductory course in logic.
Course literature: "Structural Proof Theory", Sara Negri and Jan von Plato, Cambridge U.P., 2001.
Additional material (recent articles) provided by the lecturer.
Mass Problems
Stephen Simpson (Penn State, USA) – 5 lecturesA mass problem is a set of Turing oracles. Let P and Q be mass problems; we say that P is reducible to Q if every member of Q computes a member of P. Two mass problems are said to be equivalent if each is reducible to the other. The equivalence classes are partially ordered in the obvious way; this partial ordering is easily seen to be a complete distributive lattice. We study this lattice and its sublattice obtained by restricting to mass problems of the form P = the set of all paths through T, where T is a computable subtree of the full binary tree. We present some examples of such mass problems arising from Martin-Lof randomness, effective immunity, and the Arslanov completeness criterion.
Natural Deduction: Some Recent Developments
Jan von Plato (Helsinki, Finland) – 4 lecturesStructural proof analysis in natural deduction, in contrast to sequent calculus, soon leads to very complicated considerations. This difficulty is mainly due to the complex notion of normal derivation. In recent work, what are known as "general elimination rules" have been introduced. These rules permit a simple definition of normality and a straightforward proof of normalization. They also lead to a full understanding of the relation between natural deduction and sequent calculus. The improved control on the structure of normal derivations enables, for example, proofs of underivability in intuitionistic logic that so far have been possible only through sequent calculus.
Applicative Theories and Explicit Mathematics
Reinhard Kahle (Universidade Nova de Lisboa) – 3 lecturesWe give a short introduction to the framework of explicit mathematics. It was introduced by Solomon Feferman in the 1970s in order to give a logical account to Bishop-style constructive mathematics. Soon this framework turned out to be very important for the proof-theoretic analysis of subsystems of second order arithmetic and set theory. Moreover, systems of explicit mathematics provide a logical framework for functional programming languages.
In a typical formulation of explicit mathematics one has to deal with two sorts of objects, namely operations and types. Applicative theories consist of the first order part of explicit mathematics, only, i.e., they deal with operations only. It turned out that already this applicative basis is of significant—especially proof-theoretic—interest.
The aim of the course is to present the formal framework and to discuss some of the main results in the realm of explicit mathematics.
Term-rewriting and Termination in Proof Theory
Roy Dyckhoff (St Andrews, Scotland) – 4 lectures1. Survey of work (by various people) on terminating calculi (LJT or G4ip)
Background reading: my paper in the JSL 1992.2. Survey of work on Herbelin's calculus (also called LJT...)
Background reading: my paper with Urban, JLC, to appear.3. Survey of termination via term rewriting techniques in cut elimination
Background reading: my paper with Pinto in Studia Logica.4. To be decided: possibly the latest on term rewriting in nominal logic as applied to problems such as confluence of cut-reduction systems.
Copies in PDF format of most material (Note that sometimes an inequality is missing from TTR-Dresden.pdf; it can usually be guessed. This is a feature...)
Some other things can be found on this web site, especially the first and third items.
Dependent Type Theories
Peter Aczel (Manchester, UK) – 4 lecturesAfter a quick introduction to simple type theory and its correspondence with intuitionistic implicational logic the course will develop the full Curry-Howard correspondence between predicate logic and a dependent type theory. The course will continue with a selection from a range of topics such as pure type systems, the calculus of constructions, Martin-Lof type theories, logical frameworks, etc.
Room 350 for lectures and room 357 for coffee-breaks
Computer Science Department
Hans-Grundig-Str. 25
01307 Dresden
Tel.: +49 (351) 463 38340 (Sylvia Epp, secretary)
Every day room 350 will be available for discussions until 20:00.
Rooms 106 and 108 have freely available Unix workstations (you are given a personal account).
In this period Dresden is hot and possibly windy; sometimes it rains.
See here how to reach us.
The workshop starts at 9:15 on Monday, June 23, with a brief welcome. Every day the workshop ends at 16:30.
Week 1: June 23-27, 2003
Courses MON TUE WED THU FRI 9:30-10:30 SS SS SS SS SS 10:30-10:45 b b b b b 10:45-11:45 SN SN AG SN SN 11:45-12:00 b b b b b 12:00-13:00 JL AJ JL JL AG 13:00-14:15 lunch lunch lunch lunch lunch 14:15-15:15 AJ JL AJ AJ AJ 15:15-15:30 b b b b b 15:30-16:30 AJt AJt AG AJt AG AG = lecture by Alessio Guglielmi
AJ = lecture by Achim Jung
AJt = tutorial by Achim Jung
JL = lecture by Jim Lipton
SN = lecture by Sara Negri
SS = lecture by Stephen Simpson
b = coffee break
Week 2: June 30-July 4, 2003
Courses Workshop MON TUE WED THU FRI 9:30-10:30 PA PA RD talks talks 10:30-10:45 b b b 10:45-11:45 RD RD RD 11:45-12:00 b b b 12:00-13:00 JvP JvP JvP 13:00-14:15 lunch lunch lunch lunch lunch talks
start at 13:45talks
start at 14:0014:15-15:15 PA RK JvP 15:15-15:30 b b b 15:30-16:30 RK PA RK JvP = lecture by Jan von Plato
PA = lecture by Peter Aczel
RD = lecture by Roy Dyckhoff
RK = lecture by Reinhard Kahle
b = coffee break
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 organise trips and social events.
Details on the cultural program
Some hotels and apartment agencies offer accommodations to participants. In general, you should mention the magic words `Summer School at TU Dresden´ in order to have special prices applied. All suggested places are conveniently connected by public transportation to the summer school and workshop venue.
Complete accommodations list and information on public transports
60 people registered for the summer school and workshop.
This event is organized by Paola Bruscoli, Birgit Elbl, Sylvia Epp, Bertram Fronhöfer, Axel Großmann, Alessio Guglielmi, Steffen Hölldobler, Reinhard Kahle, Aning Song, Mariana Stantcheva, Charles Stewart and the AI Institute at TU Dresden, and sponsored by Deutscher Akademischer Austausch Dienst (DAAD), IQN (Rational mobile agents and systems of agents), Graduiertenkolleg 334 (Specification of discrete processes and systems of processes by operational models and logics), Consolato Generale d'Italia - Lipsia/Italienisches Generalkonsulat in Leipzig and CoLogNet.
Back to the Calculus of Structures
Alessio Guglielmiemail