• View
• Edit
• History
• Print

TypeTheoryAndFormalizationOfMathematics

• Thursday December 11: Workshop Type theory and formalization of mathematics (in kårhuset, Ascom room)
  9:30 - 10:00 Fika
  10:00 - 11:00 Martin-Lof - Making sense of normalization by evaluation (notes available upon request)
  11:15 - 12:15 Palmgren - Variants of categories with families and their formalization PDF
  Abstract: Categories with families (cwfs) is one of the semantical structures for Martin-Löf type theory (MLTT) that is closest to the syntax of the theory. Formalizing the notion in type theory it self present some choices, whether to consider cwfs whose equality is interpreted as definitional equality in types and terms, which restricts the number of models, or is interpreted as extensional equality. The latter presents some problems of coherence. We also consider cwfs with named projections and their relation to Martin-Löf's Substitution Calculus (1992). This talk presents work in progress.
  12:15 - 13:45 Lunch
  13:45 - 14:45 Gonthier - Constructing Algebraic Numbers Attach:Gonthier.pdf
  While ordinarily algebraic numbers are introduced as a subset of the (classical) complex numbers, it is common folklore that they can also be obtained constructively. However actually constructing algebraics is not so easy, and doing so elegantly and rigorously in a formal proof system is even harder. With R. O'Connor and C. Cohen, we had to revisit constructively several topics in number theory to arrive at a satisfactory resolution. In the process we also got an answer of sorts to another ancient conundrum: isn't the Fundamental Theorem of Algebra really a theorem in Analysis?
  15:00 - 16:00 Lumsdaine - Characterising identity types of inductive types: from 1 ≠ 0 to Blakers–Massey.
  The “code-decode” method has been one of the most fruitful discoveries in the type-theoretic ("synthetic") development of homotopy theory. It extends traditional type-theoretic characterisations of identity types of inductive types (e.g. decidable equality of booleans and naturals), to similarly characterise or approximate the identity types of higher inductive types, recovering close analogues of various classical homotopy-theoretic results.
  16:00 - 16:30 Fika
  16:30 - 17:30 Rasmus Møgelberg - Topos of trees Attach:ToposofTrees.pdf