CMU Campus
Department of         Mathematical Sciences
Events People Colloquia and Seminars Conferences Centers Positions Areas of Research About the Department Alumni
Richard Statman, Professor
Ph.D., Stanford University
Office: Wean Hall 7214
Phone: 412-268-8475


My area of research can be described hierarchically as: mathematical logic, proof theory and the theory of computation, theory of programming languages (computer science), theory of functional programming, lambda calculus/ combinatory logic

Lambda calculus is the study of certain computation rules or programs. From among those programs which can be applied to arguments and return values we single out those whose execution depends only on the fact that some of the data are themselves computation rules of the same sort. It is not obvious that there are any non-trivial examples of such rules. The rich deep structure of the lambda calculus had to be discovered by Church, Bernays, Curry, Kleene and those who followed them. Since then, many distinctions have been made, such as those between applicative and functional programming, and many quite different type systems have evolved.

There is currently a great deal of research into lambda calculus by the programming language, theorem proving and symbolic computing communities. In our work we are interested in the deep structure of pure lambda calculus both with and without types. Roughly speaking our work falls into 6 general categories.

1. Typed lambda calculus and its extensions
2. Evaluation, reduction and conversion strategies
3. Combinators and combinatory algebra
4. Computability of functions and invariants
5. Functional equations and unification
6. Connections to other branches of mathematics such as semigroup theory.

Selected Publications:

  • Solution to the range problem for lazy lambda calculus and combinatory logic (with Benedetto Intrigilia), in preparation
  • The omega rule is pi-one-one complete (with Benedetto Intrigilia), TLCA 2007
  • The complexity of alpha conversion, J.S.L. Vol 72 Issue 4 2007
  • Two variables are not enough ICTCS 2005
  • The omega rule is sigma-zero-three hard (with Benedetto Intrigilia), LICS'04
  • On the lambda Y calculus, LICS '02
  • Church's lambda delta calculus, LPR '00
  • The word problem for combinators, RTA '00

IEEE Symposium on Logic in Computer Science