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:

  • A new type assignment for strongly normalizable terms, CSL 2013
  • Near semirings and lambda calculus, TLCA 2014
  • (with Bill Gunther) Reflections on a theorem of Henkin in The Life and Work of Leon Henkin Manzano et al eds, Birkhauser 2014 pps 203-216
  • A finite model property for intersection types, ITRS 2014
  • (with Benedetto Intrigila) Lambda theories allowing terms with a finite number of fixed points, MSCS July 2015
  • How to think of intersection types as Cartesian products; a converse to the BPS theorem, MFPS 2016
  • Some tweets about mockingbirds to appear in the festschrift for Ray Smullyan; Outstanding Contributions to Logic Ray Smullyan Springer-Verlag
  • Levy labels and recursive types, LFCS 2016
  • (with Benedetto Intrigila) Fixed point theorems in lambda calculus to appear in the special issue of Indagationes Mathematicae L.E.J. Brouwer, fifty years later Dirk van Dalen, Jan Willem Klop, Jan van Mill, Geurt Jongbloed eds.
  • Een aankondiging voor recursieve types in Liber Amicorum Henk Barendregt Herman Geuvers, Freek Wiedijk eds Radboud Universtity 2015
  • On the representation of semigroups and other congruences in the lambda calculus, MFPS 2016
  • The completeness of BCD for an operational semantics, PLRR 2016

IEEE Symposium on Logic in Computer Science