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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev