ProgLog Main
ProgLog Pages
edit SideBar

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 MartinLof  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 MartinLö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 MartinLö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 “codedecode” method has been one of the most fruitful discoveries in the typetheoretic ("synthetic") development of homotopy theory. It extends traditional typetheoretic 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 homotopytheoretic results. 16:00  16:30 Fika 16:30  17:30 Rasmus Møgelberg  Topos of trees Attach:ToposofTrees.pdf
