Re: [isabelle] A course based on Isabelle/HOL and some feedback...

Le 28/04/12 15:39, Makarius a écrit :
You mention OCaml occasionally in passing, as if it could be assumed as
background of French students. Is this the case? I am giving a 2-day
Isabelle/HOL tutorial in 2 weeks at Paris Sud, so it would be good to
know if OCaml can be taken for granted.

For french students, I would say yes...

What I have already learned is that Coq can *not* be taken for granted
here in France, even though international conferences on theorem proving
sometimes give a different impression.

Yes, it is true. The overall knowledge of Coq highly depends on the university where you come from. You are very much likely to be exposed in "Research" Masters (you probably know this distinction we have in France now that you are at LRI :-) ... The course that I gave was designed for "Professional" Masters... which explains that it does not put the stress on proofs tactics and so on.

Best regards,

Thomas Genet
Campus de Beaulieu, 35042 Rennes cedex, France
Tél: +33 (0) 2 99 84 73 44 E-mail: genet at

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