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

Your Answer

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

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