Announcing Isabelle2011-1 with code generation for Scala

Isabelle2011-1 is now available.

Isabelle is a generic proof assistant. It allows mathematical formulas
to be expressed in a formal language and provides tools for proving
those formulas in a logical calculus. A particular calculus is
higher-order logic (HOL), which can be thought of as a functional
language enriched with logical constructs like sets, quantifiers etc.
The code generator of Isabelle allows to turn HOL specifications into
programs in a couple of languages, including Scala – or, more exactly, a
functional subset of Scala with type classes represented by implicit
arguments.

More on that can be found in the Tutorial on Code Generation, available
in the Isabelle distribution and online at
http://isabelle.in.tum.de/dist/Isabelle2011-1/doc/codegen.pdf

Isabelle's user interface is based on jEdit and implemented in Scala itself.

You may get Isabelle2011-1 from the following mirror sites:

Cambridge (UK) http://www.cl.cam.ac.uk/research/hvg/Isabelle/
Munich (Germany) http://isabelle.in.tum.de/
Sydney (Australia) http://mirror.cse.unsw.edu.au/pub/isabelle/

Happy hacking!

Florian