Re: [isabelle] Scala code generator generates ill-typed code from subtraction of n-ary functions
-----BEGIN PGP SIGNED MESSAGE-----
2013-07-03 19:33 Florian Haftmann:
> Concerning »actively maintained«, there is somebody (namely me)
> who will look after your issue.
Thanks for your encouraging reply!
And, @Cornelius, thanks for your experience report.
> 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.
I am nowhere near an _experienced_ Scala programmer yet, but
sufficiently capable of writing wrapper functions that, e.g., convert
set[Nat] to List[Int], so this is fine with me. Replying to
@Cornelius, my application so far is small enough to only require a
few wrapper _functions_, but I'll consider your suggestion of doing
Are you suggesting that the code generator creates nicer output for
other target languages? (I'm just curious; I'm not planning to use
any other language than Scala for now.)
> 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.
For now, our applications won't be more than thin wrappers around the
generated code, providing some console or file I/O, in a medium-term
perspective maybe a GUI or web interface. But really just to obtain
input for the Isabelle-generated functions from an end user, and for
displaying the output of the Isabelle-generated functions back to the
Christoph Lange, School of Computer Science, University of Birmingham
http://cs.bham.ac.uk/~langec/, Skype duke4701
→ Intelligent Computer Mathematics, 8–12 July, Bath, UK.
→ Modular Ontologies (WoMO), 15 September, Corunna, Spain.
Submission until 12 July; http://www.iaoa.org/womo/2013.html
→ Knowledge and Experience Management, 7-9 October, Bamberg, Germany.
Submission until 15 July; http://minf.uni-bamberg.de/lwa2013/cfp/fgwm/
→ Mathematics in Computer Science Special Issue on “Enabling Domain
Experts to use Formalised Reasoning”; submission until 31 October.
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2.0.20 (GNU/Linux)
Comment: Using GnuPG with Thunderbird - http://www.enigmail.net/
-----END PGP SIGNATURE-----
This archive was generated by a fusion of
Pipermail (Mailman edition) and