Main page

Objectives and state of art

Research groups

Software

Tutorials and advanced lectures

The Types mailing list

Previous events

Organisation

Contact

Chalmers

The Programming Logic Group within the Computer Science Department at Chalmers University has participated in all the previous EU funded TYPES working groups and coordinated one of them.

The Programming Logic Group has long-standing experience and expertise in the area of Intuitionistic Type Theory and its application to programming and mechanisation of proofs. The proof assistants ALF and AGDA, with the user interface ALFA were developed by this group.

The group plans to contribute to three project objectives.

• In Proof Technology, Peter Dybjer, Patrik Jansson and Marcin Benke are working on type theory and generic programming. The group has been actively involved in starting the Cover project (Combining Verification Methods) - a collaboration between the three main research groups at the department. It is expected that the proof assistants mentioned above will play an important role in this project. Of particular interest are methods to combine testing and interactive program verificiation. The role of automatic theorem proving is also interesting.
• In Foundational Research, Thierry Coquand is collaborating with Randy Pollack from Edinburgh on type systems for dependent records. Ana Bove is interested in proof methods for termination checking. She has worked a few months at the Nijmegen site and she is still actively collaborating with Venanzio Capretta and interacting with Yves Bertot (both currently at the Sophia Antipolis site). Aarne Ranta and Bengt Nordström are currently using type theoretical ideas in the area of natural languages technology, in collaboration with the Linguistic Department at Gothenburg University.
• In Formal Mathematics, Thierry Coquand has started to interact with Bas Spitters, now employed in the Nijmegen team, on computational mathematics.

The senior members of the Programming Logic Group are

• Bengt Nordström, contact person
• Ana Bove
• Marcin Benke
• Catarina Coquand
• Thierry Coquand
• Peter Dybjer
• Patrik Jansson
• Aarne Ranta
• Jan Smith

The group organised an international Workshop on Termination and Type Theory in the fall 2002.Several members of the group have been teaching in the TYPES and APPSEM summer schools series. Last year three post docs from the LogiCal research group visiting the department. In the spring, Alexandre Miquel, from the LogiCal group in France, came to give a course on introduction to type theory.

Chalmers homepage