[isabelle-dev] Announcing Isabelle work: Access Modifiers for Scala Code Generator

[Lukas Erlacher]

Hello,

I am currently a graduate student in the second semester of the
master's course for computer science at TUM.
For the next 3 months, and possibly more, I will be employed by the
Chair for Network Architectures and Services (I8) at TUM to work on
the scala code generator in Isabelle.

Cornelius Diekmann is working there to build a library for analysis of
security properties in networks and is using Isabelle to create
verified code. My first order of work is to add access modifiers to
the scala code generator so all the not explicitly exported methods
pulled in by the code exporter are automatically marked private.

For example if I write
  export_code List.sublists in Scala
then I want
  def sublists...
but
  private def map...
because I did not export map.

In a more advanced scenario, helper functions (in this toy example
map) might only be correct under certain assumptions. Thus, a
programmer on the Scala level should not be able to accidently call
them directly.

We approached Fabian Immler and Florian Haftmann for this and they are
supportive of our plan. I will be coordinating my work with them.

Since this feature has already been implemented for the Haskell code
generator by Yukata, I'm hoping this will be straightforward and if
the maintainers are interested, the feature can be taken on into
Isabelle 2014.

I hope I am welcome here and that my work will be useful to everyone.

Best regards
Lukas Erlacher