[isabelle] Report from our Isabelle course



Dear list,

we just had the final presentation this yearâs installment of the
Isabelle course in Karlsruhe. In their final reports, the students
gave feedback, and some of the feedback pertains the general Isabelle
ecosystem, which Iâd like to share with your.

 * Some would have loved to have more tool support for style and
   analysis, i.e. some form of linter, and better ways to query the
   âcall graphâ of the lemmas.

    Such tooling is of course tricky with Isabelle, partly because of
    the âTo parse Isabelle you need to run Isabelleâ problem.

 * Some suggested that it would be nice to have the documentation
   available as a website, and not just PDFs. Websites have the
   advantage that they are searchable by Google & co, easily linkable,
   and generally more accessible than the somewhat rigid PDF format.

    I think this is a worthwhile suggestion and one that might be
    doable, at least if the TeX code producing the PDF documentation is
    structured well enough to be fed to one of the TeX-to-HTML-
    conversion tools.



By the way: We had one group that solved the final task (for a given
while language with time-counting big-step-semantics,
proveÂdeterminism, implement constant folding and propagation (without
fixed-point iteration for WHILE), prove that to be totally semantics
preserving, time-improving, idempotent and type-preserving) in only 260
lines of code, compared to 500 in the example solution and ~1200 in the
typical solution. Very impressive!

Greetings,
Joachim

ÂÂhttp://pp.ipd.kit.edu/lehre/SS2016/tba/


-- 

Dr. rer. nat. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner

Attachment: signature.asc
Description: This is a digitally signed message part



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