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



Hi!

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

I'd like to chime in on that by noting that we do a course on "Specification and Verification with Higher-Order Logic" in Isabelle/HOL as a Master's course.
Last year we set up a wiki (https://svhol.pbmichel.de) for the students, so we could dump in some knowledge about Isabelle/HOL, the proof general, HOL theory and general emacs.

It was also mainly designed for the students to contribute; the wiki is world-editable. Feel free to contribute :-)

Maybe the site is of some interested to one or the other. Regarding the above quote I'd say our FAQ - Ask Questions section might be of interest :)

Patrick Michel
Software Technology Group
University of Kaiserslautern


On 28.04.2012, at 15:39, Makarius wrote:

> 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:
>> http://www.irisa.fr/celtique/genet/ACF/
> 
> 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.
> 
> 
> 	Makarius
> 





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