W jaki sposób nazwa „Isabelle” (przysłowiowa twierdzenie) ma swoją nazwę?

11

Tytuł mówi wszystko, ale jestem ciekawy, ponieważ nie jest oczywiste, jak to się stało, że nazwano go „Isabelle”. Czy to imię pochodzi od osoby? Niektórych wyszukiwań w Google nie mogłem się dowiedzieć.

IIM
źródło
2
Czy próbowałeś zapytać na liście adresowej użytkowników Isabelle?
DW
Nie zrobiłem - sam nigdy nie korzystałem z Isabelle - czytałem tylko gazetę, która z niej skorzystała.
IIM
1
Pytanie to wydaje mi się nie na temat, ponieważ dotyczy historii artefaktu oprogramowania, a nie artefaktu CS. To powiedziawszy, opublikowano artykuły o Isabelle, więc pozwolę społeczności decydować.
Raphael
Aktualizacja Wikipedii :-)
Mark Hurd

Odpowiedzi:

9

Trochę google-fu (i moja pamięć) mówi mi, że najwyraźniej został nazwany przez Larry'ego Paulsona po córce Gerarda Hueta .

Gerard Huet jest jednym z ludzi stojących za mniej poetycko uznanym twierdzeniem Coqa .

Mały świat!

cody
źródło
1
Jak nazwa Coq jest mniej poetycka? Jest to gra słów nie mniejsza niż trzy słowa (Calculus of Constructions CoC, jeden z założycieli teorii Thierry Coquand i francuskie słowo oznaczające koguta (który jest symbolem Francji, a większość założycieli Coq to Francuzi)) .
Gilles 'SO - przestań być zły'
Nazwa Coq pewnością jest mądry (nie było dodatkowym ograniczeniem, że języki programowania akademickie zostały nazwane zwierzęcia, patrz np SML), ale nie sądzę, że jest to nieco mniej poetycki, zwłaszcza biorąc pod uwagę dodatkowy pun (w języku angielskim przynajmniej), że Wouldn postawiła poza Gerhardem Huetem na celowość.
cody