Re: [isabelle] Scala Code Generation

Le 11/08/11 15:00, Florian Haftmann a écrit :
Hi all,

since Isabelle2011 there is the possibility to generate Scala code from
HOL theories.  Some minor problems can be circumvented by a suitable
patch and will disappear in the next release.

Apart from that, is there any further feedback (positive or negative) on
code generation for Scala?  I would like to announce it on the Scala
mailing list after the next release, but for this I need some evidence
that it is really working.

Thanks for any feedback,

	Dear Florian,

as I already mentioned to you, we will use Isabelle2011 and Scala export for teaching on the second semester here at Rennes 1 University at master level. We already experimented a bit with the scala export in order to integrate formally developed components (in Isabelle) into Java software. For the moment everything is OK... but it is true that we will use only simple things: integers, strings, lists, etc... no exotic Isabelle theory :-)

Best regards,

Thomas Genet
Campus de Beaulieu, 35042 Rennes cedex, France
Tél: +33 (0) 2 99 84 73 44   E-mail: genet at

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