My name is Robert Harper, and I am a Professor of Computer Science at Carnegie Mellon University, where I have been a member of the faculty of the Computer Science Department since 1988.  My main research interest is in the application of constructive type theory to the design and implementation of programming languages and to the development of systems for mechanization of mathematics.  I’m probably best known for my work on the design and implementation of Standard ML, for the introduction of the LF logical framework, and for the development of the concept of a type-directed certifying compiler based on typed intermediate languages.  I have led research projects on computer networking, scientific computing, design and semantics of programming languages, grid computing, parallel scientific computing, mechanized meta-theory for programming languages, and on the theory of types.  I am actively engaged in both undergraduate and graduate teaching.  Most recently, I led the effort to revise the introductory curriculum in Computer Science, which is currently being rolled out.  I have written and co-authored several books, including The Definition of Standard ML, Programming in Standard ML, and, most recently, Practical Foundations for Programming Languages (which is currently available on the web in draft form).  I am an ACM Fellow, a recipient of the Allen Newell Medal for Research Excellence and the Herbert A. Simon Award for Teaching Excellence, and co-recipient of the ACM PLDI Most Influential Paper Ten Years Later award, and the IEEE LICS Test of Time Award (presented for the most influential paper twenty years after publication).

Disclaimer: The opinions expressed herein are those of the author, and should not be construed as representing the views of Carnegie Mellon University, the National Science Foundation, or any other agency or organization.


13 Responses to About

  1. hi,

    thx a lot for the blog mr. harper.

    i’m confused however.

    — your reasoning seems crystal clear to me, as far as i can judge from my few ‘observations’ as an amateur.
    like e.g. why haskell cannot provide (real) inductive reasoning: when i cannot just reason about 0 and succ n if n : nat, but have to consider (at least) one (or even more) other cases, then i also cannot really see the point.
    if it’s possible, let’s say ‘obvious’, to do it right, let’s say how to do it better, then why not?
    to me, this does not look like “taking math too serious”, but rather: “taking math serious in a useful way (= so that it Really becomes easier but not more difficult in the end)”.
    [[ as mentioned, i’m talking as an complete amateur here, not knowing too much, so if there’s something wrong with this comment/question, please excuse me ]]

    — then if this is so, why not change it? in my eyes, a scientist has the obligation to do things right the next 20 years even if he’s done it wrong the first 20. or at least to admit ‘it’ and not to keep confusing people.

    — someone mentioned something like being a better Java programmer in the end, if nothing else then at least that. But when the language does not allow doing it (really) better, there’s not much room to do so.. So, ok, might be a honourable aspiration, but a cheap one, somehow, and not really satisfying.

    so, i don’t really understand.. :/

    P.S.: your blog is good already bc one gets directed to it sooner or later, like when having an idea like:
    “hm, seems that haskell gets only good reputation, let’s see if there’s also something wrong, just in case i’m being fooled. let’s see what google gives me when typing ‘haskell flaws'”

    best regards and thx a lot once again


  2. borgauf says:

    I just dropped a MOOC course based on SML. I liked SML, but outside of the course materials, I found references and tutorials pretty thin, and often enough confusing for their divergent styles. For example, some seemed to be heavy on type, others more hand-waving. All in all, it felt too much like I was dealing with abandon-ware.

    • See sml-family.org for a constructive proof of non-abandonment of SML.

  3. Hello,
    Although ML is your FP language of choice (at least for teaching, from what I’ve gathered), I am hoping that you will write an article about the disadvantages of ML compared to other prominent functional programming languages. I ask this of you because you are both an expert in this field as well as an advocate for ML.
    Thank you

    • That’s a great suggestion! I think I’ll do it, as soon as I get the chance.

  4. […] https://existentialtype.wordpress.com/about/ О блоге Меня зовут Роберт Харпер, я один из профессоров факультета компьютерных наук университета Карнеги-Меллона. Я работаю на этом факультете с 1988 года. Основным направлением моих исследований является применение конструктивной теории типов к проектированию и реализации языков программирования а так-же к разработке систем механизации математических преобразований. Полагаю, я более всего известен благодаря своему участию в разработке и реализации языка Стандартный МЛ, введению логического фреймворка ЛФ, а так-же благодаря разработке концепции сертифицирующего компилятора управляемого типами и построенного вокруг типизированных внутренних языков. Я так-же руководил исследовательскими проектами на темы – компьютерных сетей, научных вычислений, проектирования и семантики языков программирования, грид-вычислений, параллельных научных вычислений, автоматизированной мета-теории для языков программирования, и по теории типов. Я активно участвую в обучении как студентов так и аспирантов. В последнее время я возглавляю группу, занятую пересмотром вводного курса по программированию (прим.перев. 15-150?), который преподается в настоящее время. Мною были написаны (в том числе в соавторстве) несколько книг, включая “Определение Стандартного МЛ”, “Программирование на Стандартном МЛ” и, наконец, напоследок “Практические основы языков программирования” (черновик последней доступен в интернете в настоящее время). Я являюсь членом ACM (АссоциацииВычислительнойТехники), удостоен награды Аллена Ньюэлла за совершенство в исследованиях, а так-же награды Герберта Саймона за совершенство в преподавании, был среди удостоенных награды ACM PLDI “наиболее ключевая статья даже десять лет спустя” и среди IEEE LICS “проверка временем” (за статью, остающуюся важной 12 лет после публикации). Стандартное предупреждение: Мнения, выраженные здесь и далее, являются личными мнениями автора, и не должны представляться как выражение мнения Университета Карнеги-Меллона, Национального Научного Общества, либо любого другого агенства или организации. […]

    • I’ve taken the risk of approving a comment that I blatantly cannot understand, since I don’t read a word of Russian. Let’s hope it’s appropriate! If not, please inform me, and I’ll take it down.

  5. Vijay Ganesh says:

    Dear Professor Harper,

    I recently stumbled upon your blog. I read many of the articles there, and was particularly impressed by the “Holy Trinity” article. It is beautifully crafted, as if a word-smith has gone to work.

    My own background is in logic, although more recently I have been devoting increasing amount of my time to types.

    Coming back to your article, I was surprised not to see complexity theory mentioned. It is our best attempt at understanding computation through the lens of cost.

    I guess your reasons could have been that complexity theory itself can be interpreted using logic.

    Anyways, thanks for a very inspiring post which has great clarity of thought.


    • thank you!

  6. stefjoosten says:

    It is interesting to read that you are letting freshmen learn FP as their first programming language. I applaud that idea from my own experience as a university teacher. I have been involved in a similar experience, but that was even before the invention of Haskell, in 1985-1990. We experimented with the (then commonplace) language Miranda as the first programming language for students.

    Our idea was: first you let them learn a clean way of programming (e.g. Miranda) and only then you show them programming in other languages. Very much like electronics students first learn nice-and-neat laws, such as Ohm and Kirchoff, and only then they learn to cope with all sorts of limitations, special cases etc.

    The FP course took 1 trimester and the imperative course took the second trimester.

    It surprises me that this idea is still considered new today. Our work was 25 years ago. I suppose this has to do (does it?) with the fact that FP never took on as a broadly embraced programming paradigm in practice.

    If you want more information, contact Gerrit van der Hoeven at the University of Twente. He was the project leader, and responsible for its success.

    • Abstract Type says:

      I think the only thing that is new is the emphasis on parallel computing, especially asymptotic analysis for parallelism, and the emphasis on verification. What has happened is that these topics have suddenly become politically viable, whereas previously they were not, which allowed me to convince my colleagues that the time was right to emphasize FP. The fundamentals have not changed at all, just the perception of what is important by the unenlightened. In particular I believe that the whole mania about “object-oriented programming” in the 1990’s and 2000’s was a colossal backward step, because we already had better ideas long before these were introduced so broadly. And now we are seeing people step backwards and trying to pretend that what is old is new, and that what we’ve been saying for decades is suddenly now “object-oriented”, which is the preferred way to express approval of any idea whatsoever, particularly if it is not original.

  7. Derek Wyss says:


    I am a computer science student at Hawaii Pacific University. I have been looking at some of your earlier blog entries, and I was initially inspired to want to learn SML. After looking around at some of the available tutorials on the internet though, my interest has cooled a little. The free SML tutorials are boring. Also, I may be wrong, but there doesn’t seem to be anything out there that explains how to get user input while using SML, and I find that more than a little irritating. I have been looking around at what other functional languages are out there, and I like the freely available OCaml and Erlang tutorials much better. It also seems that SML has been abandoned. So my question to you is…

    Is SML really that great? If so, why is it “dead”?

    You lay out pretty clearly why SML is the right language to teach your class in. Also, it is pretty awesome when you get an instructor who literally wrote the book on the language being taught. However, on your CMU homepage, you have a link to Successor ML which says, “Standard ML, being incapable of evolution, is dead.” Based on some of the dates on the Successor ML page, Successor ML kind of looks dead too. By linking to the Successor ML page, I assume that you think there is room for improvement with Standard ML, but it seems those improvements will not be forthcoming.

    So, when your students are done learning all of the great things to be learned by using SML like parallelism and reasoning about code, what are your expectations after that? Will they continue to use SML as a tool even though it is a dead end programming language? Should they move on to a laguage that is not a dead end – perhaps OCaml or Scala? Do you expect better functional languages to be available for your students in the future, perhaps Ωmega or Trellys. It is often put forward that using a functional programming language will make you a better progrommer overall. So maybe the idea is to take the lessons learned using SML and go forth and be a better Java programmer (similar to the way you learn Latin to be better at English)?



    • Aaron West says:

      Haskell is sometimes considered to be part of the ML family. Once a student has learned pure FP in any language, they can apply it in other languages. I might be tempted to argue for use of Haskell in preference to ML as a teaching language, but if the teacher is more comfortable with SML, then it’s probably safer to stick with that. I would also argue that OCaml is more “alive” and current than ML (as is F#), but they are so close to SML that I still think the point is nearly moot. It’s about learning the style of programming in functional programming; about learning referential transparency and equational reasoning. Minor differences in syntax shouldn’t be very important in the long-run, though I do think F# might be a bit more “fun”, because of the Visual Studio environment. Actually, why not argue for F#? It’s freely available with the Visual Studio shell, and as much as I like Linux and all its various tools, if the students have Windows laptops or desktops readily available, I think they might enjoy “Intellisense” and other features of the Visual Studio environment.

Leave a Reply

Please log in using one of these methods to post your comment:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: