Robert L. Constable
computer scientist educated under Alonso Church and Stephen Kleene.
He received his A.B. (1964) from Princeton University, his M.A (1965), and his PhD
University of Wisconsin, all in Mathematics. Currently he is the head of the Nuprl
research group in
automated reasoning and software verification at Cornell University. He served
ten years as the founding dean of the Faculty of Computing and Information Science.
His professional activities include editorships of The Computer Journal, Journal of
and Computation, and of Logical Methods in Computer Science. He serves on several
boards including for the Computer Science Departments at Columbia University,
Princeton University and Johns Hopkins University as well as for and the Michigan
School of Information. He has also held positions with research
organizations such as LICS - General Chair, NATO Summer School
at Marktoberdorf - Director, Microsoft - Faculty Fellows Committee.
He is an ACM Fellow and was granted the John Simon Guggenheim Fellowship
and the Outstanding Educator Award.
Professor Constable's research interests include formal methods, applied logic
and programming language theory. He is known as one of the founders of computational
type theory and of Nuprl, one of the first type theory based theorem provers. He has written three
books on programming logics and type theories and has supervised 42 PhD students thus far.
Each week Scholarpedia recognizes a different contributing author by featuring a short bio of them on the home page.