Minisymposium on Type Theory and Foundations -------------------------------------------- Thursday 15 January 2009 Venue: Room Å11167, Ångströmlaboratoriet, Uppsala University 9.30 - 10.45 Maria Emilia Maietti "A two level theory for constructive mathematics" Abstract: In joint work with G. Sambin [1], when looking for a minimalist foundation for constructive mathematics we ended up claiming the need of a two level theory for that. We give an example of such a two level foundation from [2] and we discuss its consistency with combinations of formal Church thesis, choice principles and Monotone Bar Induction by means of realizability models. [1]"Toward a minimalist foundation for constructive mathematics", M.E.M and G. Sambin in ''From Sets and Types to Topology and Analysis: Practicable Foundations for Constructive Mathematics", (L. Crosilla and P. Schuster eds.) Oxford University Press, 2005. [2] "A minimalist two-level foundation for constructive mathematics", M.E.M. to appear in APAL, 2009 11.00 - 12.15 Andreas Abel "Typed Applicative Structures and Normalization by Evaluation" Abstract: Normalization by evaluation is a technique to compute the full beta-normal form of lambda-terms. In the first step, terms are interpreted in some value domain, which corresponds to computing a semantic weak head normal form. In the second step, values are reified, i.e., converted back to terms which are actually normal forms. During reification, evaluation under binders takes place. In this talk, I will give a tutorial on normalization by evaluation for the simply-typed lambda-calculus. I review interpretation of lambda-terms into an applicative structure and then define a simple type-directed reification which returns eta-long beta-normal forms. I sketch the proof of soundness and completeness which involves constructions of Kripke logical relations. The proof is generic enough to account for related results, like weak beta-(eta-)normalization. 13.45 - 15.00 Peter Dybjer "Program testing and constructive validity" Abstract: In this talk I will discuss the connection between Martin-Löf's meaning explanations for intuitionistic type theory and program testing. First I give a short overview of the historical development of the ideas behind the meaning explanations. Then I explain the connection with program testing. Finally, I will mention the possibility of pursuing the testing point of view for some other logical systems. 15.15-16.30 Olov Wilander "Another LCCC of partial setoids" In a paper by Barthe, Capretta, and Pons, a seemingly exhaustive list of notions of partial setoids is investigated. One of the notions found unsuitable there is modified to yield a LCCC not equivalent to the category of (total) setoids, but where all the constructions are chosen. Time permitting, some investigation of the categorical logic will also be presented.