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, 2016 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, 2016 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, 2016 at 0:08
  • 1
    $\begingroup$ Wikipedia updated :-) $\endgroup$
    – Mark Hurd
    Apr 28, 2016 at 7:28

1 Answer 1


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!

  • 2
    $\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, 2016 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, 2016 at 13:28

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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