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.
$\begingroup$
$\endgroup$
4
-
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$– IIMApr 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 HurdApr 28, 2016 at 7:28
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
2
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$– codyApr 13, 2016 at 13:28