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.
Campus de Beaulieu, 35042 Rennes cedex, France
Tél: +33 (0) 2 99 84 73 44 E-mail: genet at irisa.fr
This archive was generated by a fusion of
Pipermail (Mailman edition) and