*To*: Christoph LANGE <math.semantic.web at gmail.com>*Subject*: Re: [isabelle] Scala code generator generates ill-typed code from subtraction of n-ary functions*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Wed, 03 Jul 2013 20:33:03 +0200*Cc*: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <51D3205A.5030303@gmail.com>*Organization*: TU Munich*References*: <51D3205A.5030303@gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:17.0) Gecko/20130623 Thunderbird/17.0.7

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

**Follow-Ups**:

**References**:

- Previous by Date: [isabelle] Scala code generator generates ill-typed code from subtraction of n-ary functions
- Next by Date: Re: [isabelle] Scala code generator generates ill-typed code from subtraction of n-ary functions
- Previous by Thread: [isabelle] Scala code generator generates ill-typed code from subtraction of n-ary functions
- Next by Thread: Re: [isabelle] Scala code generator generates ill-typed code from subtraction of n-ary functions
- Cl-isabelle-users July 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list