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 more.

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 be simplistic.


	Makarius


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.