Up: Cooperating sites
Previous: INRIA-Sophia
Kent
The Functional Programming Group at the University of Kent has a long history of involvement with dependdent type theories. Thompson is the author of an early (1990) introduction to the area and Hanna is the implementor of a dependently-typed system, Veritas, used in early hardware verification work. Current interests of the group centre around building systems to make functional programming systems more usable. These include work on refactoring in FP languages such as Haskell, foundations of functional programming type systems, and Computer algebra and verification.
The group will make contributions to the following objectives:
- Correctness of computer programs: to work on functional programming and dependent types.
- Formal mathematics and mathematics education: to continue work in verified computational mathematics with Therese Hardin's group at LIP6, Paris, who are, in turn, collaborators with the Coq group, the Paris Sud and INRIA sites of the current proposal.
Dependently typed systems provide a major challenge for implementors and system designers alike. The group also aims to extend the projects in refactoring and visual programming to embrace dependent types, in collaboration with groups at Gothenburg and elsewhere. This will also link with the Cover project at Gothenburg.
The senior members of the Functional Programming Group are
- Simon Thompson, contact person
- Keith Hanna
- Stefan Kahrs
- Claus Reinke
Bengt Nordström 2005-09-22