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.