LOGIKSEMINARIET STOCKHOLM-UPPSALA 25 ÅR

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

9.00 - 10.00 Peter Dybjer, Chalmers

A category-theoretic approach to type-checking dependent types

10.30 - 11.30 Alexandre Buisse, Chalmers

Formalizing (categorical models of) type theory inside type theory

11.45 - 12.45 Richard Garner, Uppsala

Two-dimensional models of type theory

14.30 - 15.30 Erik Palmgren, Uppsala

Type universes and ramifications

15.45 - 16.45 Thierry Coquand, Chalmers

Type theory and functional programming

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 with
extra 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.