Re: [isabelle] Where to learn about HOL vs FOL?
On Wed, 6 Feb 2013, Yannick Duchêne (Hibou57) wrote:
Le Wed, 06 Feb 2013 15:41:05 +0100, Makarius <makarius at sketis.net> a écrit:
I have pointed out further nasty tricks of OCaml occasionally, where you
simply cannot trust your eyes reading the OCaml source. Some LRI guys are
particularly good at playing such tricks and proud of it.
What is “LRI” please?
French habit of making long complicated expressions short: Laboratoire de
Recherche en Informatique, i.e. the CS lab at Paris Sud.
The coffee room of the lab is sometimes an exchange point for the latest
OCaml tricks -- there are many power users of it. Historically, the lab
was also one of the originators of Coq, but that is now mainly done at LIX
and PPS/Pir2 -- yet more odd abbreviations (you are French yourself, so
you should know).
And of course, Coq is not untrustable just because it is using OCaml.
The French colleagues understand the problems and made their homework, but
it also introduces complexities. People like Bruno Barras could tell you
So maybe that is now the point for Mark Adams to move this never-ending
thread to coq-club to see how they react about high-end provers having to
This archive was generated by a fusion of
Pipermail (Mailman edition) and