JSSymposium

Symposium on Programming and Constructive Mathematics

dedicated to Jan Smith in connection with his 60th birthday Gothenburg, 31 May, 2010

Venue: Chalmerska huset, Södra Hamngatan 11, Gothenburgh.

Preliminary Program

09.30 Peter Aczel: Rudimentary Constructive Set Theory

Constructive Set Theory (CST) provides an extensional purely set-theoretical, but constructively acceptable, setting for the formalisation of the practice of constructive mathematics. Rudimentary CST (RCST) is a very weak part of CST that is, nevertheless, strong enough to express many standard non-numerical set-theoretical constructions. I will describe RCST and its metatheory and some arithmetical extensions.

10.15 Herman Jervell: What is a function?

What is a function from natural numbers to natural numbers - developed in ordinary first order logic ? We argue that it is exactly the Kalmar elementary functions, and show that these are exactly the functions where the use of cut helps in getting short proofs that these functions work as they should.

11.00 Coffee
11.45 Per Martin-Löf: Spreads and choice sequences in type theory

A notion of sheaf model of type theory over an underlying spread of choice sequences will be proposed.

12.30 Lunch.
14.00 Giovanni Sambin: Levels of Abstraction

Interspersed with some memories from the 80s and 90s, I will argue that different levels of abstraction are present by nature in mathematics and in theoretical computer science. Under this perspective, I will briefly analyse some hot issues in constructive mathematics, as intensional vs extensional aspects, axiomatic definitions, abstract algebraic structures, existence of points, choice sequences and bar induction, automatic implementation, etc., and show that each of them acquires a clearer status, if not a solution.

14.45 Coffee
15.30 Erik Palmgren: Sets, setoids and groupoids

When formalising constructive mathematics in Martin-Löf type theory it is standard to use setoids (types with equivalence relations) to interpret sets. The notion of preset is well captured by a type equipped with its identity type as equivalence relation. However when it comes to families of sets it seems that there is a choice between proof relevant index sets (groupoids) and proof irrelevant index set (setoids). We aim to discuss these issues and the relation to the groupoid model of type theory by Hofmann and Streicher.

16.15 end of last talk
16.30 (16.39) -- 17.02 (17.11) Tram nr 11 to Saltholmen
17.20 -- 17.43 Boat to Styrsö Skäret
Dinner at Restaurant Skäret
20.37 -- 21.12 Boat Skäret -- Saltholmen (later boat at 21.56)
21.29 -- 21.59 Tram nr 11 Saltholmen -- Brunnsparken