The title says it all, but I'm curious because it isn't obvious how a theorem prover came to be named 'Isabelle'. Was it named for a person? I couldn't find out by some Google searches.

  • 2
    $\begingroup$ Have you tried asking on a Isabelle users mailing list? $\endgroup$
    – D.W.
    Apr 5 '16 at 20:51
  • $\begingroup$ I haven't - I've never used Isabelle myself - I've only read a paper that used it. $\endgroup$
    – IIM
    Apr 6 '16 at 11:35
  • 1
    $\begingroup$ This question strikes me to be offtopic as it is about the history of a software artifact, not a CS artifact. That said, articles have been published about Isabelle so I'll let the community decide. $\endgroup$
    – Raphael
    Apr 13 '16 at 0:08
  • 1
    $\begingroup$ Wikipedia updated :-) $\endgroup$
    – Mark Hurd
    Apr 28 '16 at 7:28

A little google-fu (and my own memory) tells me it was apparently named by Larry Paulson after Gerard Huet's daughter.

Gerard Huet happens to be one of the people behind the less poetically named Coq theorem prover.

Small world!

  • 1
    $\begingroup$ How is the name Coq less poetic? It's a pun on no less than three words (the Calculus of Constructions CoC, one of the founders of the theory Thierry Coquand, and the French word for rooster (which is an emblem of France, and most of the Coq founders were French)). $\endgroup$ Apr 13 '16 at 1:20
  • $\begingroup$ The Coq name is certainly clever (there was an additional constraint that academic programing languages were named after an animal, see e.g. Ocaml) but I do think it's a bit less poetic, especially given the additional pun (in English at least) that I wouldn't put beyond Gerhard Huet to be intentional. $\endgroup$
    – cody
    Apr 13 '16 at 13:28

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.