The Department of Computer Science and Engineering is a shared department between Chalmers Tekniska Högskolan, Chalmers University of Technology, and Göteborg University. The Programming Logic Group of the Department is one of the pioneers in a series of European TYPES projects, working on type theory and its applications to program verification and computer-assisted mathematics. The current TYPES project (Types for Proofs and Programs, FP6-2002-IST-C) is coordinated by the Chalmers group. The Language Technology group is a spin-off of this group, focusing on the development of natural language processing tools based on type theory. The system GF (Grammatical Framework) developed in this group permits the definition of multilingual systems based on language-independent semantics expressed in type theory. GF was applied in the WebALT project to implement multilingual translations of mathematical exercises. The group has close contacts with the Departments of Linguistics and Swedish, and has also been involved in the spoken-language applications of GF, in the project TALK (Talk and Look: Tools for Ambient Linguistic Knowledge, IST-507802).