Carnegie Mellon University

Richard Statman


7214 Wean Hall
Department of Mathematical Sciences
Carnegie Mellon University
5000 Forbes Avenue
Pittsburgh, PA 15213

P: 412-268-8475


Richard Statman


M.A., University of Cambridge
Ph.D., Stanford University


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.

Select Publications

Statman, R., (2013). A new type assignment for strongly normalizable terms. CSL.

Statman, R., (2014). Near semirings and lambda calculus. TLCA.

Statman, R., (2014). A finite model property for intersection types. ITRS.

Statman, R., (2015). Taming the wild ant-lion. MSCS.

Statman, R., (2016). Levy labels and recursive types. LFCS.

Statman, R., (2016). How to think of intersection types as Cartesian products ; a converse to the BPS theorem. MFPS.

Statman, R. (2016). On the representation of semigroups and other congruences in the lambda calculus. MFPS.

Statman, R. (2017). The completeness of BCD for an operational semantics. LFCS.

Statman, R. and Intrigila, B. (2018). Fixed point theorem in lambda calculus. Indagationes Mathematicae. 450-458.

Statman, R. (2018). Some tweets about mockingbirds in Ray Smullyan on Self Reference Mel Fitting and Brian Rayman eds. Springer-Verlag. 113-122.

Statman, R. (2018). Minimal Backus FP is Turing complete. FLOC.

Statman, R. (2018). Sets of terms with a given intersection type. FLOC.

IEEE Symposium on Logic in Computer Science