Petri Mäenpää has investigated the methodology of program derivation in type theory, and developed a type-theoretical grammar of programming languages. He has also applied the grammar to programsynthesis that is based on a complete, purely type-theoretical description of the syntax and semantics of the target programming language.Moreover, the syntax comprises not only abstract but also concrete syntax.
Sara Negri has been working on formal topology and its applications to contructive analysis, partly in collaboration with Göteborg. She has also established connections between domain theory and type theory, via representations within formal topology of basic structures of domain theory like continuous lattices.
Aarne Ranta has been developing a grammar of informal mathematical language based on his earlier research on type theory and linguistics.This work has resulted in a Haskell implementation that makes it possible to interact with proof editors in six natural languages. Experimental versions of this interface are being built in collaboration with Göteborg and with Durham. As an example of program development using proof editing in natural language, Matti Kinnunen has written a natural-language interface to regular expressions.
Jan von Plato has developed further his axiomatization of systems of constructive geometry, where the presence of constructions with conditions leads to dependent typing. These systems have been used as case studies in Ranta's work, and in systems of automated theorem proving.