13:30--15:00 Constructive mathematics and computer programming - some background, Peter Dybjer (Chalmers University of Technology) Abstract: In 1979 the Swedish logician Per Martin-Löf wrote a landmark paper entitled "Constructive mathematics and computer programming". In this paper he proposes a new language which can be used both by mathematicians and by programmers. In fact, he takes the view that mathematics (if viewed "constructively") is the same thing as computer programming - a rather novel and controversial point of view. In his language "intuitionistic type type theory" you can do several things. The programmer can of course write programs, but also specifications which explain what a program is supposed to do, without actually saying how it should perform the task. While programming a type-checker makes sure that the program satisfies its specification. Moreover, a mathematician can state a theorem, and then write a proof of it in the language. The type-checker can then check that the proof is indeed a correct proof of the theorem. Martin-Löf's ideas have spread widely, and are now pursued by many computer scientists from all over the world, including Sweden and Japan. Among other things, a practical version of Martin-Löf's language called "Agda" is the focus of a collaboration between Chalmers University of Technology in Sweden and the Advanced Institute of Industrial Science and Technology (AIST) in Japan. In this talk I will give a general introduction to this area. I will do my best to provide a broad view and not assume too much background in order to make it interesting to science students in general, not only to mathematicians and computer scientists. It is my belief that the ideas presented will have an impact on the teaching of mathematics and computing to science students in the future. For example, in an article in Nature from 2006 it is predicted that computer science will play a similar role for science in the future as mathematics has done in the past.SLIDE1 Photo

SLIDE2 Photo

Photos

10:00--10:45 Program testing and constructive validity, Peter Dybjer (Chalmers University of Technology)

Abstract: In this talk I shall argue that program testing provides the basis for mathematical truth, and that mathematics is an empirical science. This point of view is the result of an analysis of Martin-Löf's meaning explanations for intuitionistic type theory, where the judgements of type theory are viewed as conjectures which can be tested in order to be corroborated or refuted. One consequence is a new perspective of hypothetical judgments, since tests for such judgments need methods for generating inputs. Among other things, we need to generate function input. The continuity principle is relevant here and it follows that the alleged impredicativity of functionals can be rejected. Furthermore, our testing semantics suggests that we should only allow the formation of identity types over decidable types. At the end we turn to impredicative type theory, and discuss possible testing semantics for such theories. In particular we propose that testing for impredicative type theory should be based on the evaluation of open expressions rather than of closed expressions as for predicative type theory. SLIDE PhotoAbstract:

10:50--11:35 Towards a computational interpretation of parametricity,

Jean-Philippe Bernardy (Chalmers University of Technology), Guilhem Moulin (Chalmers University of Technology)

Reynold's abstraction theorem has recently been extended to λ-calculi with dependent types. We will show how this theorem can be internalized (that is, both expressed and proved in the calculus itself) in an extension of the Calculus of Constructions with a special parametricity rule (with a computational content).

SLIDE Photo1 Photo2

11:40--12:25 Dependent Polynomial Functors for Inductive Families, Makoto Hamana (Gunma University)

Abstract:

It is well-known that every algebraic datatype is characterised as the initial algebra of a polynomial functor on sets.

We extend the characterisation to more advanced datatypes: Dybjer's Inductive Families. Specifically, we show that Inductive Families are characterised as initial algebras of dependent polynomial functors. We also show that the differentiation of dependent polynomial functors provides zipper data structures on Inductive Families. This is joint work with Marcelo Fiore.

SLIDE Photo

-----------------------------------------------------------------------------------------------------