This site contains wikipages for the department of computer science and engineering at Chalmers and GU. 
CS /
JSSymposiumSymposium on Programming and Constructive Mathematicsdedicated to Jan Smith in connection with his 60th birthday Gothenburg, 31 May, 2010 Venue: Chalmerska huset, Södra Hamngatan 11, Gothenburgh. Preliminary Program
Constructive Set Theory (CST) provides an extensional purely settheoretical, 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 nonnumerical settheoretical constructions. I will describe RCST and its metatheory and some arithmetical extensions.
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.
A notion of sheaf model of type theory over an underlying spread of choice sequences will be proposed.
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.
When formalising constructive mathematics in MartinLö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.
