firas med följande
föredrag den 26 mars i sal Å2002, Ångströmlaboratoriet,
Uppsala.

9.00 - 10.00 Peter Dybjer,
Chalmers

10.30 - 11.30 Alexandre
Buisse, Chalmers

11.45 - 12.45 Richard Garner,
Uppsala

14.30 - 15.30 Erik Palmgren,
Uppsala

15.45 - 16.45 Thierry
Coquand, Chalmers

ABSTRACTS

PETER DYBJER: An
algebraic presentation of Martin-Löf's logical framework

is given
which is based on the notion of a category with families withextra structure. We present a type-checking

algorithm for the normal forms of this theory, and sketch how it

gives rise to an initial category with families with

extra structure. In this way we obtain a purely algebraic

formulation of the correctness of the type-checking algorithm which

provides the core of proof assistants for intuitionistic type

theory.

ALEXANDRE BUISSE: We
investigate the possible formalization of categorical metatheory
of

constructive type theory in (an extension of) itself, using
the notion of``internal type theory''. The model chosen is categories with families, which

model the most basic part of dependent type theory. We will discuss how to

formalize them inside type theory, and also how to formalize the proof that

categories with finite limits, another model of type theory, can be seen as

categories with families. The formalization was carried out with the proof

assistant coq, and we will present it in detail.

RICHARD GARNER: There
is a well-known correspondence between locally cartesian closed
categories and extensional type theories with the eta-rule for
dependent products. We sketch a way in which this correspondence may
be generalised to one between two-dimensional locally cartesian closed
categories and certain "two-dimensional" intensional type theories. We
also indicate how any intensional type theory gives rise to a
two-dimensional intensional type theory by an internal groupoid
construction.

ERIK PALMGREN: We
examine the natural interpretation of a ramified type hierarchy into
Martin-Löf type theory with an infinite sequence of universes. It
is shown that under this interpretation a useful special case of
Russell's reducibility axiom is valid. This is enough to make the type
hierarchy usable for development of constructive
mathematics.