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