Symposium on Semantics and Logics of Programs, 5 June 2013

This symposium is dedicated to Peter Dybjer to celebrate his 60th birthday

Venue: 10:an, Vasaparken, Gothenburg (enter the university building, take the stairs to the left to the second floor)

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 set-theoretical 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 Martin-Lö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 COLOG-88. 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: Induction-Recursion - 20 years later. In this talk we first start to review the prehistory of induction-recursion, starting with the Backhouse 1988 "Do-it-yourself-type-theory", 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 inductive-recursive definitions was introduced. We consider the TLCA paper by Dybjer and the author, in which a closed axiomatisation of induction-recursion 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 induction-induction by Fredrik Forsberg and the author, and a categorical reformulation of induction-recursion by Neil Ghani et al., which generalises induction-recursion 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 coinduction-corecursion 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,