The focus of this research group is on logic in computer science, with particular interest in lambda calculus and functional programming, types, constructive mathematics, proof theory, linear logic, and semantics.
Our group is equipped with the usual array of workstations, backed up by a complex of turbocharged multitape Turing Machines, a prototype high-speed optimal reduction machine, and a type-directed partial evaluator.
As of November 1998, we are running a bimonthly seminar on programming language theory and implementation, tentatively devoted to topics in linear logic and extracting computational content from classical proofs.