This symposium is dedicated to Peter Dybjer to celebrate his 60th birthday
Preliminary program:
 9:30 Peter Aczel, Manchester: The Structure Identity Principle in Set Theory and Type Theory. The Structure Identity Principle (SIP) states that Isomorphic structures are structurally identical. After discussing SIP in the setting of settheoretical mathematical practice and formulating a precise general notion of mathematical structure I will prove a theorem of Homotopy Type Theory. The theorem states that a strong form of SIP for that notion of mathematical structure, as represented in intensional dependent type theory, is a consequence of a new axiom for type theory, Voevodsky's Univalence Axiom. The strong form of SIP expresses that isomorphic structures are identical.
 10:30 Refreshments
 11:15 Per MartinLöf, Stockholm: The infinity Axioms of Nonstandard Type Theory. Nonstandard type theory was introduced 25 years ago in a paper entitled Mathematics of Infinity, published in COLOG88. The purpose of my talk is to give a new formulation of the crucial Infinity axioms, which distinguish it from standard type theory, and to prove their equivalence with a certain saturation, or completion, principle.
 12:15 Lunch
 13:45 Phil Scott, Ottawa: Presheaf Models for a Quantum Lambda Calculus. In recent work with Octavio Malherbe and Peter Selinger, we investigated presheaf models of quantum computing, in particular for the quantum lambda calculus of Selinger and Valiron. We shall describe both abstract and concrete models for these, as well as similar, theories.
 14:45 Thierry Coquand, Gothenburg: Sheaf models of type theory. The notion of category with families, introduced by Peter Dybjer, provides an elegant formulation of type theory as a generalized algebraic theory. We use this concept to describe sheaf models of dependent type theory. As an application, we show that Markov's Principle cannot be proved in dependent type theory.
 15:45 Refreshments
 16:15 Anton Setzer, Swansea: InductionRecursion  20 years later. In this talk we first start to review the prehistory of inductionrecursion, starting with the Backhouse 1988 "Doityourselftypetheory", Peter Dybjer's 1989/90 schemata for inductive definitions, and Thierry Coquand and Christine Paulin's inductively defined types. These development led then to the May 1992 Munich talk and the June 1992 TYPES talk in which a general schema for inductiverecursive definitions was introduced. We consider the TLCA paper by Dybjer and the author, in which a closed axiomatisation of inductionrecursion was presented, and its reformulation in the APAL paper on initial algebras. We investigate applications to generic programming. Then we look at recent developments, the formulation of inductioninduction by Fredrik Forsberg and the author, and a categorical reformulation of inductionrecursion by Neil Ghani et al., which generalises inductionrecursion to a much larger variety of situations. Finally we discuss open problems such as how to extend induction recursion to include the Mahlo principle and what a notion of coinductioncorecursion could be.
 17:15 end of last talk
18:00 Dinner: Fiskekrogen (for those who have signed up for it)
Birthday wishes to Peter has been sent from:  Alley Stoughton, MIT Lincoln Laboratory,
 Paul Levy, Birmingham,

