Dr. Robert L. Constable

From Scholarpedia
Curator of ScholarpediaCurator Index: 1(Redirected from User:Constable)
Jump to: navigation, search

    Department of Computer Science, Cornell University, Ithaca, NY

    Curator and author

    Icon author.png

    FEATURED AUTHOR

    Robert-Constable.jpg

    SCHOLARPEDIA ARTICLES

    Computational type theory

    Scholarpedia, 4(2):7618. (2009).

    Robert Constable

    Robert L. Constable is a

    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 (1968) from 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 Cornell for 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 Logic and Computation, and of Logical Methods in Computer Science. He serves on several advisory 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.

    Personal tools
    Namespaces

    Variants
    Actions
    Navigation
    Focal areas
    Activity
    Tools