Topos Theory Seminar
Fall 2004

Organizers: Lars Birkedal, birkedal@itu.dk, Room 4C 15, 7218 5280

Carsten Butz, butz@itu.dk, Room 4C 14, 7218 5274

This is a Ph.D. seminar in which we study aspects of topos theory relevant to computer science. After having read material from Peter Johnstone's opus Sketches of an Elephant: A Topos Theory Compendium, Lambek/Scott's Introduction to higher order categorical logic, Mac Lane/Moerdijk's Sheaves in Geometry and Logic we plan to continue with a semester on realizability toposes (without assuming too much knowledge of the material covered in previous semesters to allow new students to participate). Additional material can be found at Jaap van Oosten's page with links to recent articles on realizability and at Lars Birkedal's (somewhat dated) online bibliography on realizability.

The main goal of the seminar this Fall is to get an understanding of various realizability toposes and how theses are constructed from so-called triposes. In particular, we'll address recent attempts to create realizability toposes for Godel's dialectica interpretation. Further off-line topics could include how realizability toposes may be constructed and analyzed using exact completions; a deeper analysis of subcategories of realizablity toposes; how one may understand Krivine's notion of realizabilty as a tripos / topos; application of realizability models in semantics of programming languages; etc.

Readings will include (excerpts from some of):

[1] Introduction to Constructive Logic and Mathematics by Thomas Streicher
[2] J.M.E. Hyland. The effective topos. In A.S. Troelstra and D. Van Dalen, editors, The L.E.J. Brouwer Centenary Symposium, pages 165-216. North Holland Publishing Company, 1982.
[3] J.M.E. Hyland, P.T. Johnstone, and A.M. Pitts. Tripos theory. Math. Proc. Camb. Phil. Soc., 88:205-232, 1980.
[4] A.M. Pitts. The Theory of Triposes. PhD thesis, Cambridge University, 1981.
[5] L. Birkedal. Developing theories of types and computability via realizability. Electronic Notes in Theoretical Computer Science, 34, 2000.
[6] J. Avigad and S. Feferman. Gödel's functional ("Dialectica") interpretation in S. Buss ed., The Handbook of Proof Theory, North-Holland, 337-405, 1999.
[7] L. Birkedal. Notes on the Dialectica Topos.
[8] J. M. E. Hyland: Variations on Realizability: Realizing the Propositional Axiom of Choice. Mathematical Structures in Computer Science 12(3): 295-317 (2002) 20
[9] J. M. E. Hyland: Proof theory in the abstract. Ann. Pure Appl. Logic 114(1-3): 43-78. 2002.
[10] T. Streicher. A Semantic Version of the Diller-Nahm variant of Godel's Dialectica Interpretation.
[11] L. Birkedal and J. van Oosten. Relative and modified relative realizability. Annals of Pure and Applied Logic, 118(1-2):115-132, 2002.
[12] J. van Oosten. The modified realizability topos. Journal of Pure and Applied Algebra, 116:273-289, 1997.
[13] J. van Oosten. History of Realizability
[14] A.M. Pitts. Tripos Theory in Retrospect. Mathematical Structures in Computer Science 12(2002) 265-279.
[15] G. Rosolini. About Modest Sets. International Journal of Foundations of Computer Science, 1, 1990.

To gain credit for this 7.5 ECTS seminar you have to participate actively in the discussions. Moreover, you have to take responsibility for at least one topic, stretching usually over more than a week.

Meeting time: We meet on Fridays, 14:00--16:00, Room 2A 14 (except Oct. 1 where it is in 2A 20)

Participants:

(birkedal@itu.dk, butz@itu.dk, volodya@itu.dk, hilde@itu.dk, mogel@itu.dk, noah@itu.dk, rusmus@itu.dk, biering@itu.dk, m98mb@math.ku.dk)

We will not go through [13] J. van Oosten. History of Realizability at the seminar, but yoo should read it off-line.

Schedule:

Date Speaker Reading

Fri Sep 10 LB Sec 0--8 in [1]

Fri Sep 17 RLP Sec 9--11 in [1]

Fri Sep 24 BB Sec 12--14 in [1]

Fri Oct 1 LB [14] + Ch. 5 in [5] (Bonus: [3] + [4])

Fri Oct 8 REM [2]

Thu Oct 14 REM [2], continued (Bonus: [15])

Fri Oct 29 BB Ch. 6 in [5]

Fri Nov 12 CB [12]

Fri Nov 19 RLP [11]

Fri Dec 3 RLP [11], continued

Fri Dec 10 BB part of [6]

Fri Dec 17 LB [9], [7], [10]n

Organizers:	Lars Birkedal, birkedal@itu.dk, Room 4C 15, 7218 5280
	Carsten Butz, butz@itu.dk, Room 4C 14, 7218 5274

Date			Speaker	Reading
Fri	Sep	10	LB	Sec 0--8 in [1]
Fri	Sep	17	RLP	Sec 9--11 in [1]
Fri	Sep	24	BB	Sec 12--14 in [1]
Fri	Oct	1	LB	[14] + Ch. 5 in [5] (Bonus: [3] + [4])
Fri	Oct	8	REM	[2]
Thu	Oct	14	REM	[2], continued (Bonus: [15])
Fri	Oct	29	BB	Ch. 6 in [5]
Fri	Nov	12	CB	[12]
Fri	Nov	19	RLP	[11]
Fri	Dec	3	RLP	[11], continued
Fri	Dec	10	BB	part of [6]
Fri	Dec	17	LB	[9], [7], [10]n

Topos Theory Seminar Fall 2004

Topos Theory Seminar
Fall 2004