Richard Statman is an American logician and computer scientist at Carnegie Mellon University, known for foundational work on the computational complexity of type theory and lambda calculus. His results on the complexity of normalization and decidability problems in typed lambda calculi have been influential in both proof theory and theoretical computer science.
Proved that the simply typed lambda calculus has non-elementary recursive complexity (Statman's theorem)
Established key results on the computational complexity of normalization in type systems
Contributed to understanding the relationship between logical provability and computational tractability
Advanced the study of the lambda calculus and its connections to proof theory