Models of Dependent Type Theory - Advanced Semantics Seminar
Fall 2008

Organizer:

Lars Birkedal, Room 4C 15, 7218 5280

This is a Ph.D.-seminar in which we study some aspects of semantics of programming langauges and type theories relevant to computer science. This semester we focus on models of dependent type theories, including the calculus of inductive constructions and its realization in the Coq system, leading up to realizability models of Hoare Type Theory.

Readings will include (excerpts from some of):

• B. Nordstroem et. al.: Programming in Martin Loef's Type Theory.
• Coquand and Paulin-Mohring: Inductively Defined Types.
• P. Dybjer: Internal Type Theory.
• M. Hofmann: Syntax and Semantics of Dependent Types.
• B. Jacobs: Categorical Logic and Type Theory.
• B. Jacobs: Comprehension Categories and the Semantics of Type Dependency. Theoretical Computer Science 107, 1993.
• Z. Luo: Computation and Reasoning.
• A.M. Pitts: Categorical Logic, In Handbook of Logic in Computer Science (Vol. VI). Oxford Univ. Press.
• Sambin and Smith: Twenty-Five Years of Type Theory.
• T. Streicher: Investigations into Intentional Type Theory.
• Coq Theory
• W. Phoa: An introduction to fibrations, topos theory, the effective topos and modest sets.
• R.L. Petersen, L. Birkedal, A. Nanevski, G. Morrisett A Realizability Model of Hoare Type Theory.

To gain credit for this 7 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, 10:00--12:00, Room 4A 05. starting Sep. 10, 2008.

Tentative Schedule:

Date			Speaker	Reading
Fri	Sep	12	LB	Intro: Hofmann Sec. 1-2.
Fri	Sep	19	AB	CwF: Hofmann Sec. 3.1 - 3.3 + Dybjer/Buisse paper.
Fri	Sep	26	KS	PCA's + w-Sets + Modest sets / PERs: Jacobs: Sections 1.1 - 1.2.
Fri	Oct	03	LB	Fibrations: Jacobs: Sections 1.3-1.10
Fri	Oct	10	LB	Fibrations and CwFs: Jacobs: Sections 10.1 - 10.5 + Exercise 10.4.6.
Fri	Oct	17		Cancelled (Fall break)
Fri	Oct	24		Ph.D. school of Logics and Semantics of State
Fri	Oct	31	LB/TD>	Assemblies and modest sets as Closed Comprehension Categories (Jacobs)
Fri	Nov	07	KS + AB	Additional verifications of the realizability model of DTT
Fri	Nov	14	LB	Models of FhoDTT, generic objects, internal categories (Jacobs, Ch. 7, 11)
Fri	Nov	21	LB	cancelled
Fri	Nov	28	LB	Intersection and Union Types in DTT (no additional readings)
Fri	Dec	5	LB	Models of dependent predicate logic (Jacobs, Ch. 11)
Fri	Dec	12	LB	A Realizability Model of HTT (paper by Petersen et. al.)