CSE dept.
This site contains wikipages for the department of computer science and engineering at Chalmers and GU.
edit SideBar

A homepage for the Decidability Algorithms workgroup.
Involved sites:
Participants:
 Thierry Coquand, professor, CSE.
 David Wahlstedt, post doctor, PLATOS.
 Anders Mörtberg, Phd student, CSE.
 Bassel Mannaa, Phd student, CSE.
 Stevan Andjelkovic, Master Student, CSE.
Funded research projects:
 European Union's 7th Framework Programme
ForMath (see wiki page), grant agreement no. 243847. Led by Thierry Coquand, with Phd student Anders Mörtberg.
 ERC Advanced grant project 247219.
Led by Thierry Coquand, with Phd student Bassel Mannaa.
 The Swedish Research Council
Postdoc position, registration number 2008:6902, David Wahlstedt. A summary of this project can be found here.
Brief summary:
The aim of this collaboration is to get a better understanding of some decision procedures involving infinite domains, and their constructive justifications.
Seminar series:
To begin, our activity consists of a miniseminar series. The following topics have been addressed so far:
 May 25, 2010
David Wahlstedt The sizechange principle and the classical justification of its decision procedure. The sizechange principle for program termination, introduced 2001 to the functional programming community by Lee, Jones and benAmram, is a classification of terminating recursive computation rules. It generalises lexicographical termination, and its decision algorithm is easy to implement (although it is computationally expensive). We describe this property and its decision algorithm, whose justification uses the infinite version of Ramsey's Theorem.
 June 15, 2010
Bassel Mannaa Sizechange termination and Büchi Automata.
 August 27, 2010
Anders Mörtberg Quantifier Elimination and Algebraically Closed Fields.
 September 20, 2020
(held as a logic seminar at PLATOS) David Walhstedt Some Ramseylike theorems in constructive logic and Brouwer's thesis. I am going to discuss some ideas about how to deal with Ramseylike theorems in some constructive frameworks, and some aspects concerning Brouwer's thesis on bars. I will present two different constructive interpretations of Ramsey's theorem, by Theirry Coquand, and Vim Weldman and Marc Bezem, respectively. Using these ideas, we aim to reason constructively about termination of recursively defined programs.
Other topics to address:
 S1S: secondorder monadic theory of successors
 LTL
