Seminar on Theories of Proofs, Types and Computation (BLT-seminariet)

This seminar series is planned to run for the academic year 2007/2008. It will mainly be devoted to presentation of classical and new material in proof theory, lambda calculus and type theory.

10 Sept. 2007: Olov Wilander, Structural proof theory, part I. Time and place: 15.15, room 4003.
17 Sept.: Olov Wilander, Structural proof theory, part II. Time and place: 15.15, room 11167.
24 Sept.: Olov Wilander, Structural proof theory, part III. Time and place: 15.15, room 11167
Presentation of some chapters from the book Structural Proof Theory (Cambridge University Press 2001) by Sara Negri and Jan von Plato.
1 Oct.: Richard Garner, On linear logic. Time and place: 15.15, room 4003.
8 Oct.: Richard Garner, On linear logic (cont.) Time and place: 15.15, room 4003.
Some recommended reading material
15 Oct. No seminar. We recommend Joachim Parrow's talk on the pi-calculus at the Stockholm-Uppsala Logic seminar on 17 October.
18-28 Jan. 2008. Mini course on models of dependent type theory
Lectures by Erik Palmgren:
- Friday 18 Jan. 13.15-15, room Å11167
  Some references for the lecture
  - F.W. Lawvere. Functorial semantics of algebraic theories and Some algebraic problems in the context of functorial semantics of algebraic theories. Ph.D. thesis, Columbia University, 1963. Reprinted in Theory and Applications of Categories.
  - A. Kock and G.E. Reyes. Doctrines in Categorical Logic, In: Handbook in Mathematical Logic, J. Barwise, ed. North-Holland 1977.
  - M. Hofmann. Syntax and semantics of dependent types. In: Semantics of Logics of Computation, P. Dybjer and A. Pitts, eds., Cambridge University Press. 1997. Preprint version
  - N.G. de Bruijn. Telescopic Mappings in Typed Lambda Calculus. Information and Computation 91(1991), 189-204.
- Monday 21 Jan. 15.15-17, room Å4003.
- Thursday 24 Jan. 13.15-15, room Å12167
  Some references for the lecture
  - P. Martin-Löf. Intuitionistic Type Theory. Notes by Giovanni Sambin. Bibliopolis 1984.
  - P. Martin-Löf. About models for intuitionistic type theories and the notion of definitional equality. Proceedings of the Third Scandinavian Logic Symposium (Univ. Uppsala, Uppsala, 1973), pp. 81--109. Stud. Logic Found. Math., Vol. 82, North-Holland, Amsterdam, 1975.
- Monday 28 Jan. 15.15-17, room Å11167
Feb. 4: Richard Garner, The groupoid model of type theory. Time and place: 15.15-17 room Å64119,
Abstract: We will describe Hofmann and Streicher's groupoid model of type theory and examine which aspects of it which are "intensional", and which are "extensional". This will mainly draw upon the article "The groupoid interpretation of type theory" in "Proceedings of the meeting Twenty-five years of constructive type theory"; a preprint version of which may be found at http://www.tcs.informatik.uni-muenchen.de/~mhofmann/venedig.dvi.gz
April 14: Anton Hedin, Bevisbarhetslogik. Tid och plats: 15.15-17 rum Å12167.
Abstract: Vi kommer att beskriva och undersöka modallogiken GL som korrekt karaktäriserar egenskaperna hos bevisbarhet och konsistens för första ordningens Peano-Aritmetik. Några centrala resultat som tas upp är Löbs Sats, de Jongh-Sambins fixpunktsats och Solovays resultat om aritmetisk fullständighet för GL. Jag kommer främst följa G. Boolos bok "The Logic of Provability" (1993). Två översiktsartiklar som finns tillgängliga på nätet är "Provability Logic" av Artemov-Beklemishev, och "The Logic of Provability" av Japaridze-de Jongh.
April 21: Anton Hedin, Bevisbarhetslogik (forts.) Tid och plats: 15.15-17 rum Å11167.

We aim to hold the seminars on Mondays 15.15 but it may occasionally be necessary to schedule it on other days of the week. Forthcoming subjects include dynamical proofs and "Real PCF".

For PhD students it will be possible to gain course credits by participating and presenting material.

This page is http://www2.math.uu.se/~palmgren/ptc

April 16, 2008, Erik Palmgren