Re: [isabelle] A course based on Isabelle/HOL and some feedback...
On Thu, 26 Apr 2012, Thomas Genet wrote:
This course was designed for our "professional" master students i.e.
that will end up developpers and not for "research" master students that
will end up in PhD.
The page of this course is here:
I have looked a bit through the course material. What is always
interesting is to see what users get as "survival kit" -- it provides some
hints what are the fine points that can be improved in the system itself,
for people getting exposed to it the first time.
The introduction of sledgehammer to "Solve theorems in the Cloud" is also
nice. Someone told me he always explains the algebraic law of
associativity in terms of the Google Map-Reduce framework :-)
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.
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and