Keywords: Constructive Logic, Type Theory, Category Theory, Lambda calculus, Quantum Computing, Certified Correct Programs main research interest is the application of constructive logic in Computer Science.An example of a constructive logic is Type Theory Type Theory is at the same time a programming language and a logic: propositions correspond to types and proofs to programs. Current research centers on theoretical aspects of Type Theory but also on the construction of elegant and efficient implementations of type theoretic languages. An example of this is the Epigram system, currently under development in Nottingham, which we use to develop programs which are correct by construction. Dr. Altenkirch's research covers applications of Category Theory as a formalism to concisely express abstract properties of mathematical constructions in Computer Science and the investigation of typed lambda calculi as a foundation of (functional) programming languages and Type Theory.