Re: [isabelle] Scala code generator generates ill-typed code from subtraction of n-ary functions



Hi Christoph,

> (BTW, is the Scala code generator actively maintained?  That would be
> great, because our main selling point in using Scala as an output target
> is to demonstrate that such code can easily be integrated with
> business-ready software.  This is work in the context of formalising
> auctions, see
> http://www.cs.bham.ac.uk/research/projects/formare/code/auction-theory/,
> so we need to convince people who may never heard of SML, OCaml and
> Haskell, but have heard of Java.)

Concerning »actively maintained«, there is somebody (namely me) who will
look after your issue.  I welcome your effort to carry Isabelle out of
the ML/Haskell subculture, but there is one caveat: the code generator
for Scala translates HOL's calculus into a functional Scala program
without attempting any transformation to idiomize it towards Scala as
written by experienced Scala programmes.  For illustration, have a look
at the generated code.  I never heard of any reports how feasible the
code is to incorporate in bigger Scala applications.

Stay tuned,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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