March 2009 - Haskell - Haskell.org

Re: Formal verification of high-level language implementation of critical software?
by David von Oheimb 20 Mar '09

20 Mar '09

Hello, thanks again to all who have responded to the request I sent on Feb 9. We got a couple of really good pointers and inspiring discussions. As requested by Bruce Watson, below I reproduce them for he benefit of all. Cheers, David Prof.Dr. Bruce W. Watson wrote: > Hi David, I'm sorry to say that I don't have the answers for you, > but coming from Eindhoven, I'm also hoping that someone will a good > response to you. If they do, will you summarize for this group? > Thanks and best regards to you, Bruce. *********************************************************************** Jan Jürjens wrote: > Hi again, > > you should have a look at Andy's work using F-sharp if you don't already know it. > > Jan Andy Gordon (MSR) wrote: > Hi David, > > The work Jan is referring to involved a suite of verification tools for F# Inserted by DvO: http://research.microsoft.com/en-us/um/cambridge/projects/fsharp/default.as… > programs called the CVK (Crypto Verification Kit). > See http://research.microsoft.com/cvk for an overview. > We have done formal verification of self-written F# programs for the CardSpace and TLS protocols, for example. The paper on CardSpace is here. > http://research.microsoft.com/en-us/um/people/adg/Publications/details.htm#… > The TLS implementation is here: > http://www.msr-inria.inria.fr/projects/sec/fs2cv/tlsimpl.pdf > > Regards, > > Andy *********************************************************************** John Matthews wrote: > Hi David, > > You posted a question a month back on the Haskell mailing list about > whether any software components have been written in a high level > language that have also been formally verified. I can think of a few: > > * There have been lots of software programs written in ACL2's first > order logic, which also happens to be a subset of Common Lisp. > > * NICTA's L4.Verified project uses Haskell to write an executable high > level model of their L4 microkernel. But they end up writing the actual > application in C and proving refinement, so that may not be what you are > looking for. > > * At Galois we have developed a domain specific functional language > called Cryptol for specifying cryptographic algorithms like DES and AES. > Cryptol is a purely functional language with compilers for VHDL, C, and > Haskell. Cryptol also comes with formal methods tools, including a a > MiniSat-based equivalence checker, a translator to Berkeley's ABC > equivalence checker, and a prototype translator to Isabelle. You can > find out more about Cryptol here: > > http://www.cryptol.net > > * We also developed a small monadic imperative language in Isabelle/HOL > for writing a security-critical cross-domain disk block access > controller. We proved safety and data separation properties about the > controller, and in fact the data separation proof method was inspired in > part by your ESORICS 2004 paper! inserted by DvO: http://david.von-oheimb.de/cs/papers/Noninfluence.html > We then wrote a simple translator from our monadic Isabelle/HOL subset to C. > > My colleague Paul Graunke actually carried out the work on this project, > I mainly acted as an Isabelle/HOL consultant. Paul published an experience > report at the System Software Verification workshop (SSV'08), titled > "Verified Safety and Information Flow of a Block Device". > > > * Levent Erkok and I wrote a joint paper with Alex Krauss, Florian > Haftmann, and Lukas Bulwahn in TPHOLs 2008 titled "Imperative Functional > Programming in Isabelle/HOL", inserted by DvO: http://web.cecs.pdx.edu/~jmatthew/papers/TPHOLs08.pdf > where we showed how to model a > Haskell-style state monad with first-class polymorphic heap references > and mutable arrays. Isabelle can then generate efficient imperative > Haskell, SML, and OCaml code for programs written in this monad. The > case studies include an efficient SAT checker and an imperative bytecode > verifier for Jinja, both of which were verified. [...] > > All the best, > -john *********************************************************************** Eric Verhulst wrote: > > Dear Mr. Oheimb, > > I am not really surprised about this observation. Higher level languages > provide more abstraction and most programming errors are due to the > nitty-gritty details of the implementation. When using a language like C, > one should be aware that the language is basically a form of a higher level > assembler exposing the hardware to the program. In addition, it has a > "dirty" syntax resulting in about 14O MISRA rules + 50 non-documented ones. > Why not change the language instead? > > But performance is often the issue and hence C is often used. Small code > size also means less power and less dead code, the latter also being safety > and security issues. In my personal view, it is hence a fallacy to say that > higher level languages are the solution. HLL contribute but a clean and > hence simple semantic model and a clean syntax are probably of higher > interest than a high level language that carries too much complexity and > overhead. > > Our own experience developing a network centric RTOS using formal modeling > also proved that the architecture is an important factor that is often > overlooked. While the initial set-up was to use formal modeling mainly for > verifying the software, it was used from the beginning for developing the > architecture and the functionality. The result was a big surprise. While the > team had more than ten years experience developing a similar RTOS in the > traditional way, the resulting architecture was much more straightforward > and clean, resulting in a code size that was 5 to 1O times smaller. The > architecture was also much safer (no risk of buffer overflow) and much more > scalable. The initial design phase took about 18 months but we had running > code in just 2 weeks. Later on, most issues were related to hardware issues > e.g. when developing drivers. > > My personal view is that for software like an RTOS, high level languages are > not really suitable. But for application I believe that code writing should > be avoided at all cost by using code generators that start from user defined > models, eventually complemented by formal provers (although it is early days > for such tools). An example is Matlab/simulink, at least in the domain of > e.g. algorithms. Another promising approach is to use languages (like B) > that allow incremental refinement with formal model checking in parallel. > Once such a design is complete, the risk of introducing errors even when > recoding into C is much lower than when writing by hand. > Hence, we should see these modeling tools like HLL. Nevertheless, for > educational purposes, such HLLs should be used a lot more often as they help > to learn to think in an abstract way (while most software engineers are > immediately influenced by their prior implementations and patterns.) Once > they master this, they will also write better programs in C. > > For more information about the project see www.altreonic.com and > www.openlicensesociety.org. The product is called OpenComRTOS. > > Best regards, > > Eric Verhulst *********************************************************************** Gerwin Klein wrote [translated]: > our seL4 kernel of course! It is written in Haskell and verified, > then re-implemented in C, optimized, and verified (the latter is > not yet finished, but just 6-7 weeks to go). I responded: Cool! Having a look at the picture and description at http://ertos.org/research/l4.verified/ is seems that the verification relation between the Haskell prototype and the actual code is not the usual one, where one would have (security/access control) objectives, against to which one verifies the HLD, against to which one verifies the LLD which is the Haskell implementation, against to which one verifies the optimized C implementation, right? Why did you use at the LLD level an automatically translated C version of the Haskell prototype? Gerwin Klein responded: > Greg Kimberly wrote: >> L4.verified does look interesting. >> >> Is the reason that Haskell version is not part of the proof chain because >> the "Automatic Translation" from Haskell to C is problematic from a proof >> perspective? > > The translation from Haskell to C in this case is not automatic, the C code is > completely hand-written. It follows the structure of the Haskell code closely, > but it is hand-optimised and very close to the bare metal. It is a real, > high-performance microkernel, competitive in performance with L4::Pistachio > and the current commercial OKL4 releases on ARM by Open Kernel Labs. > These are the fastest microkernels in the world. > > Greg Kimberly wrote: >> If that's the case, what would it take to fix that? > > Having completed about 60% of the C proofs, we think, we might have been able to generate "boring" parts of the C kernel from Haskell, but for this extremely performance-critical application, there will always be a lot of manual tweaking involved, so it is unclear if we could get rid of this step usefully. > > Some parts of the current kernel (packed bitfield data structures in tagged unions) are automatically generated, with automatically generated implementation proofs, but not from Haskell directly. The data structures have their own specification language specifying hardware layout etc. This technique is used in other L4 kernels as well (without the proofs), because implementers don't trust the compiler to get packed bitfields right. > > It turns out, though, that the Haskell <-> C proof is the smallest of the big proof steps in this project. We were careful to shift all deep semantic reasoning to the upper level so that really only syntactic reasoning and optimisations remain. > > If the application is not a microkernel, but an application on top of a microkernel, the picture might look quite different. Depending on how large a trusted computing base your are willing to live with, you could run Haskell directly on seL4 (we have a project going on that ports Haskell to bare seL4). You would still have the Haskell compiler and runtime in the TCB, but we think that Haskell is good for application level programming. That means you would only be proving things on the Haskell level, not on C. Much more convenient and efficient. > > I believe the guys from Galois Inc in the US (John Matthews et al) might have similar views on this. Gerwin Klein responded: > (see also other email). The C version is not automatically translated, it is carefully hand-crafted. In this project, we see the Haskell prototype as an executable specification. The performance difference is enormous (we never intended the Haskell prototype to be fast, so no thought whatsoever went into optimising it). > > David von Oheimb wrote: >> Good to hear that at least for the application level you believe a >> relatively easily verifiable HLL implementation is efficient enough. >> >> No doubt that the translation to the lowest level (down from the LLD) is >> manual for efficiency reasons. Sorry that I put my question slightly >> wrong. http://ertos.org/research/l4.verified/ states: >> >>> The next level up, the low-level design, is a detailed, executable >>> specification of the intended behaviour of the C implementation. >>> This executable specification is derived automatically from a prototype >>> of the kernel, developed in the seL4 project. The prototype was written >>> in the high-level, functional programming language Haskell >> >> So the LLD is not written in C (as I wrongly assumed above) but in some >> other executable language (Isabelle/HOL), as mentioned in section 4.7 of >> http://ertos.org/publications/papers/Klein_08.pdf) my question should >> have read: Why did you use at the LLD level not the Haskell prototype >> itself, but an automatically translated version of it? > > Yes, I should have been clearer on that. We implemented a prototype in Haskell and then translated it automatically into Isabelle/HOL. This is necessary firstly just because Haskell is not any kind of direct input format of Isabelle. Also, the translation forced us to stay within a subset of Haskell that maps nicely to HOL (Haskell as any real language has too many features). > > > >>> In this project, we see the Haskell >>> prototype as an executable specification. The performance difference is >>> enormous (we never intended the Haskell prototype to be fast, so no >>> thought whatsoever went into optimising it). >> >> Still I do not understand which was the main part of my question, namely >> why according to http://ertos.org/research/l4.verified/ your Haskell >> reference implementation is not directly in the usual verification >> chain. > > It cannot be, you can always only verify translations of programs unless you write them directly in the theorem prover (Konrad Slind et al have some nice work on compiling HOL programs directly into assembly). We make a qualitative distinction between the translation Isabelle <-> Haskell and Isabelle <-> C, because we did not have to care about the correctness of the former, but we do care about the correctness of the latter. We therefore kept Isabelle <-> C absolutely minimal and as syntactic as possible. It is really more parsing C into Isabelle than really doing any translation. Formally, both of them are translations, though. > > There is no reason that Isabelle <-> Haskell has to be a big translation step. In fact TUM and NICTA have some student projects on precisely a better, sound translation mechanism for Haskell into Isabelle. > > >> I am actually confused by what you wrote in the other email: >> >>> It turns out, though, that the Haskell <-> C proof is the smallest of the big >>> proof steps in this project. >> >> which seems to contradict http://ertos.org/research/l4.verified/ as it >> suggests that the Haskell version itself is in the verification chain. > > Sorry, I tend to shorten "the Isabelle translation of the Haskell prototype" to just "Haskell" too often. I can see that it was confusing. Did it now become clear, though? > > >> So as stated above I wonder why you use an independent executable LLD >> rather than the Prototype written in HLL (here Haskell). >> (You could also have used the Haskell prototype in between the HLD and >> LLD or in between the LLD and the hand-written C code, but this would >> add an extra (presumably superfluous) node in the verification chain.) > > No, it's actually just not possible. Isabelle does not understand Haskell (there is no theorem prover that does), it's always a translation (possibly a very small translation step). Our LLD is not independent, though. It's the product of the automatic translation. It's Haskell parsed into Isabelle if you want, although in this case there was quite a bit of transformation going on. I wrote: Maybe you have also seen on the Haskell mailing list the response of Eric Verhulst <eric.verhulst(a)openlicensesociety.org>: [see above] Gerwin Klein responded: >> Eric Verhulst wrote: >>> I am not really surprised about this observation. Higher level languages >>> provide more abstraction and most programming errors are due to the >>> nitty-gritty details of the implementation. When using a language like C, >>> one should be aware that the language is basically a form of a higher level >>> assembler exposing the hardware to the program. > > I completely agree, that's why we're using it as the kernel implementation language. For most things on top of the kernel it might not be as good a choice, though. Much nicer to work in something like Haskell directly. > >> Eric Verhulst wrote: >>> In addition, it has a "dirty" syntax resulting in about 14O MISRA rules + 50 non-documented ones. > > We solve this by accepting only a true subset of C into the theorem prover. This can be made large enough to do kernel programming comfortably. It still has a lot of dirty semantic constructs that kernel programmers like to use, but that's the whole point of using it. > > David von Oheimb wrote: >> I guess you mean not only as input to the theorem prover, but also for >> the actual kernel code. This is certainly very helpful for the cleanness >> of the code and lowers the verification burden. > > Yes, absolutely. Although the kernel programmers did not necessary like all parts of the restriction, they tend to agree that it produced cleaner code. > > David von Oheimb wrote: >> I agree one cannot use HLL for very performance critical systems. >> But how about using a HLLs as form of (executable) formal model / LLD? > > Modulo a (possibly very small) translation step into the logic of the theorem prover, that's what we are advocating. > > David von Oheimb wrote: >> This, actually includes part of the answer to my above question: The LLD >> is an Isabelle/HOL model (which is isomorphic to the Haskell prototype). > > Yes! > > David von Oheimb wrote: >> In this way you avoid having the semantics of Haskell directly in the >> verification chain, but you have it indirectly (and not really formally) >> because of the automatic translation between the Haskell prototype and >> the Isabelle/HOL version of it. Therefore, the Haskell prototype is, >> strictly speaking, not an authoritative specification but the technical >> inspiration for the LLD in Isabelle/HOL. > > Exactly. If you want to build more directly on the HLL, the translation step becomes part of your trusted tool chain and you have to invest some work into making sure that it is sound. This is clearly worthwhile, though, and would be a once-for-all effort. > > David von Oheimb wrote: >> I presume the HLD is also in Isabelle/HOL. Despite your general >> bottom-up process, wouldn't it also make sense to have the HLD influence >> the LLD (and still get something useful, but hopefully more elegant)? > > That did indeed happen. We started with the LLD, but we developed the HLD concurrently (lagging slightly behind, but giving input into new iterations). Some generalisations/restrictions become more obvious when you abstract from implementation data structures. > > >> Eric Verhulst wrote: >>> But performance is often the issue and hence C is often used. Small code >>> size also means less power and less dead code, the latter also being safety >>> and security issues. In my personal view, it is hence a fallacy to say that >>> higher level languages are the solution. HLL contribute but a clean and >>> hence simple semantic model and a clean syntax are probably of higher >>> interest than a high level language that carries too much complexity and >>> overhead. > > This depends on the abstraction level of the application, I'd say. For the RTOS/microkernel level, I agree. Too much overhead is involved in using a language like Haskell directly. We used it to describe the semantics, not the actual implementation. > >> Eric Verhulst wrote: >>> Our own experience developing a network centric RTOS using formal modeling >>> also proved that the architecture is an important factor that is often >>> overlooked. While the initial set-up was to use formal modeling mainly for >>> verifying the software, it was used from the beginning for developing the >>> architecture and the functionality. The result was a big surprise. While the >>> team had more than ten years experience developing a similar RTOS in the >>> traditional way, the resulting architecture was much more straightforward >>> and clean, resulting in a code size that was 5 to 1O times smaller. The >>> architecture was also much safer (no risk of buffer overflow) and much more >>> scalable. The initial design phase took about 18 months but we had running >>> code in just 2 weeks. Later on, most issues were related to hardware issues >>> e.g. when developing drivers. > > Absolutely the same experience here. We used Haskell as the formal modelling language, because the kernel design team was more comfortable with it than with Isabelle/HOL directly, but the difference is almost syntactic only. We have had a very rapid, iterative design cycle with new features often being implemented in less than a day. > >> Eric Verhulst wrote: >>> My personal view is that for software like an RTOS, high level languages are >>> not really suitable. But for application I believe that code writing should >>> be avoided at all cost by using code generators that start from user defined >>> models, eventually complemented by formal provers (although it is early days >>> for such tools). An example is Matlab/simulink, at least in the domain of >>> e.g. algorithms. Another promising approach is to use languages (like B) >>> that allow incremental refinement with formal model checking in parallel. >>> Once such a design is complete, the risk of introducing errors even when >>> recoding into C is much lower than when writing by hand. >>> Hence, we should see these modeling tools like HLL. Nevertheless, for >>> educational purposes, such HLLs should be used a lot more often as they help >>> to learn to think in an abstract way (while most software engineers are >>> immediately influenced by their prior implementations and patterns.) Once >>> they master this, they will also write better programs in C. > > I'd even go further and say that there are HLL now that are directly suitable for application use. We tend to use Haskell, because there is a big research group at UNSW doing work on it, but I'm sure there are more. > > David von Oheimb wrote: >> Do you second his view about the benefits of a formal HLD, in his case >> TLA+/TLC according to http://www.openlicensesociety.org/drupal55/node/9 > > A formal HLD is definitely beneficial in my view. It all depends a bit on the development process you are using. Our kernel design team was used to a bottom-up process and there is no reason this cannot be supported by formal verification -- we started with the LLD and developed the HLD in parallel. I would guess that the most important aspect of all this was that we found a formal language (here Haskell) that the *kernel design team* was comfortable with. *They* need to design the kernel, they were experienced kernel designers and programmers and new to formal modelling. They had help from us formal guys, but they did most of the LLD modelling. If we (the formal guys) had designed the kernel it would be much more elegant and much more useless. > > David von Oheimb wrote: >> Unfortunately they did not verify the C code against that model. In >> order to do that, it seems that an implementation in a HLL like Haskell >> would be a good intermediate step, wouldn't it? > > I think so. If you already have the model, it doesn't need to be a programming language. It could be logic directly if the team is comfortable with using it. > > David von Oheimb wrote: >> Yes, and this would avoid bringing the semantics of the HLL into play. > > True. I wrote: Taking into account that future hardware architectures are multicore machines which are hard to program manually - Greg Kimberly writes: > The idea that C is a good representation of what's really going down at the hardware > level is obviously very compelling when you care about performance. But I wonder how > the coming world of high-number multi-core changes that? Are we entering a world where > the cost of maintaining cache coherence becomes more important than a close correspondence > to a register machine? Functional languages, with their lack of shared state, might be > a better model then. Might C ironically become considered "too far" from the hardware > to be a good choice? :-) Do you see a chance that on multicore systems, future compilers for HLLs are (on average, for large chunks of code) smarter than hand-crafted C/assembly code, such that they can be used even for performance critical code close to the system level, maybe even OS implementation? Gerwin Klein responded: > I would agree that they will be much smarter than C compilers, but at the lowest level of software like the kernel, you still need to know precisely what's going on. Too much of the safety and correctness depends on it and there smarter is not better. It's bad enough if the kernel implementers are smart (almost always means harder proofs..). HLLs also tend to rely on OS services to implement their primitives. My current feeling is still that you want to keep the kernel close to bare metal with something like C, but I would expect even more benefit from HLLs on the application and OS component level for multi core. > > All this is not to say that C is in any way a perfect language, not even for OS implementation for which it was basically developed. In my view an ideal OS implementation language would have a modern, safe type system possibly with a controlled way of "breaking" it for hardware/performance (but breaking it in a way that produces clear and simple proof obligations), no or extremely minimal required run-time, language constructs for mapping data structures to hardware layouts precisely (even C sucks in this respect), and a very clean semantics. And it shouldn't have all these "features" from the 60s like goto etc, of course.. > Greg continued writing: > And to give some idea of why you might expect a greater performance-driven interest in FL's > in the presence of very-multi-core hardware, check out the recent article in Queue about > the experience of an IBM team building a general purpose STM (soft trans memory) system: > http://queue.acm.org/detail.cfm?id=1454466 > > Basically the cost of read/write barriers are a big problem. You can see the cost > of the read barriers in particular in the detailed perf analyses. From the summary: > "Based on our results, we believe that the road ahead for STM is quite challenging. > Lowering the overhead of STM to a point where it is generally appealing is a difficult > task, and significantly better results have to be demonstrated. If we could stress > a single direction for further research, it is the elimination of dynamically > unnecessary read and write barriers-possibly the single most powerful lever toward > further reduction of STM overheads. Given the difficulty of similar problems explored > by the research community such as alias analysis, escape analysis, and so on, this > may be an uphill battle. Because the argument for TM hinges upon its simplicity and > productivity benefits, we are deeply skeptical of any proposed solutions to > performance problems that require extra work by the programmer" > > So when they call out "elimination of dynamically unnecessary read and write > barriers-possibly the single most powerful lever toward further reduction of STM > overheads" -- it leads one to think about that being precisely the sort of thing > a powerful type system and pure functional approach would seem to be ideally > suited to helping. Perhaps functional programming comes under the "extra work > by the programmer" category :-) > (Note the comment below the article specifically wondering about Haskell's STM.) Unfortunately I do not have the time to look at the above in detail; Are there are others who might do or already have an opinion/insight in this issue? Greg continued writing: > So if folks can find a way to make writing correct programs more verifiable in > FL's the performance issue might very well be a non-issue in a few years.... Wouldn't this be great! Greg also wrote: > Still, I clearly need to look at current practice in code generators (from models). > Though I imagine they still involve even larger space/time compromises than using > HLL's relative to coding in C. So I'm a bit surprised at Mr. Verhulst's enthusiasm > for them as compared the HLL's. It might be a case of the grass being greener on the > other side of the fence, I think. It seems to me that Mr. Verhulst would also be fine with HLLs as a formal model, and that for very performance critical code he is just dissatisfied with the efficiency of compilers and code generators, and therefore prefers (any) formal model that this manually translated to C for efficiency, right? Gerwin Klein responded: > Sounds like it. I might add, that for us it's not just about the efficiency (although that is a big factor), but also about knowing precisely how things map to the hardware. Gerwin Klein wrote: > All this is not to say that C is in any way a perfect language, not even > for OS implementation for which it was basically developed. In my view > an ideal OS implementation language would have a modern, safe type > system possibly with a controlled way of "breaking" it for > hardware/performance (but breaking it in a way that produces clear and > simple proof obligations), no or extremely minimal required run-time, > language constructs for mapping data structures to hardware layouts > precisely (even C sucks in this respect), and a very clean semantics. > And it shouldn't have all these "features" from the 60s like goto etc, > of course.. This is obviously why you, and others, use some strict subset of C. Just a pity that neither of them has become a widely accepted coding standard, or even better, evolved into a new, clean version of C. Do you happen to know Scala, and what you think about it? http://www.scala-lang.org/node/25 Gerwin Klein responded: > I haven't used it extensively, but I like it as a language. Makarius is using it for Isabelle quite a bit these days, he might have more insight. *********************************************************************** Grit Denker wrote: > David, > One thing that comes to mind is the work from Mark-Oliver Stehr and > Carolyn Talcott. > In particular, I think they formalized in Maude a secure group protocol > and did some verification on it. > > See http://formal.cs.uiuc.edu/stehr/cliques_eng.html > If you need more info, contact Mark-Oliver Stehr at stehr(a)csl.sri.com > > John Rushby should have a lot more stories about successful use of > FM.Maybe there is something on http://fm.csl.sri.com/ > > grit *********************************************************************** Lars-Henrik Eriksson wrote: > Hi, > > I carried out a formal verification of a Prolog program 10 years ago > while I was working at Industrilogik L4i AB, a Swedish formal methods > consultancy which was acquired by Prover Technology (www.prover.com) > some years ago. The program was a front end to a SAT solver and > converted a formula in a first order language with finite domains to a > propositional logic formula. The conversion was slightly tricky since it > included several simplification steps. The program was just over 500 > lines in size (excluding comments and blank lines). > > The verified program was going to be used as part of a commercial formal > verification tool and the client (now Bombardier Transportation Rail > Control Solutions) wanted some assurance that the tool worked correctly. > > I used Robert Stärk's Logic Program Theorem Prover > (http://www.inf.ethz.ch/personal/staerk/lptp.html) As this was a > commercial project, there was no report written on the verification work > as such. As far as I remember, Stärk's LPTP system worked quite well. > > Best regards, > > Lars-Henrik Eriksson, PhD, Senior Lecturer > Computing Science, Dept. of Information Technology, Uppsala University, Sweden *********************************************************************** Amine Chaieb wrote: > Hi, > > Maybe not that "big" components, but we verified formally (in > Isabelle/HOL) some decision procedure implementations (mainly quantifier > elimination for linear real, integer arithmetic and their combination). > Using Isabelle's push button Technology you transform the formally > Isabelle/HOL implementation in to SML, Ocaml or Haskell. > > Here are some pointers: > > http://www.cl.cam.ac.uk/~ac638/pubs/pdf/mir.pdf > http://www.cl.cam.ac.uk/~ac638/pubs/pdf/frpar.pdf > http://www.cl.cam.ac.uk/~ac638/pubs/pdf/linear.pdf > > Best wishes, > Amine. *********************************************************************** Niklas Holsti wrote: > Hello David, > > I don't know if by "such a language" you mean specifically > functional/logic languages, but in case not: You probably know about the > Tokeener software, > http://www.adacore.com/home/gnatpro/tokeneer/ > which is implemented in SPARK Ada. Not a functional language, but one in > which data flow is controlled and verified, using the SPARK Examiner > toolset. > > Regards, > > Niklas Holsti > Tidorum Ltd *********************************************************************** David von Oheimb wrote: > Dear all, > > at Siemens Corporate Technology we are currently doing a study with > Boeing on how to enhance assurance of open-source security-critical > software components like OpenSSL. Methods considered range from standard > static analysis tools to formal verification. > > One observation is that the higher the programming language used is, > the less likely programming mistakes are, and the easier a formal model > can be obtained and the more likely it is to be faithful and verifiable. > In this sense, implementations e.g. in a functional/logic programming > language would be ideal. > > Are you aware of any (security critical or other) software component > that has been implemented in such a high-level language and has been > formally verified? Any quick pointers etc. are appreciated. > > Thanks, > David v.Oheimb > > +------------------------------------------------------------------<><-+ > | Dr. David von Oheimb Senior Research Scientist | > | Siemens AG, CT IC 3 Phone : +49 89 636 41173 | > | Otto-Hahn-Ring 6 Fax : +49 89 636 48000 | > | 81730 München Mobile: +49 171 8677 885 | > | Germany E-Mail: David.von.Oheimb(a)siemens.com | > | http://scd.siemens.de/db4/lookUp?tcgid=Z000ECRO http://ddvo.net/ | > +----------------------------------------------------------------------+ > > _______________________________________________ fortia mailing list fortia(a)fmeurope.org http://fmeurope.hosting.west.nl/mailman/listinfo/fortia

1 0

ANNOUNCE: game-tree - a library for searching game trees
by Colin Paul Adams 20 Mar '09

20 Mar '09

I've uploaded game-tree 0.1.0.0 to hackage. This library provides a class for dynamic game trees, and purely functional algorithms for searching them. I'm using it in a program that I am writing to play the game of Chu Shogi (see http://www.colina.demon.co.uk/chu.html for a description of the game, not the program). -- Colin Adams Preston Lancashire

1 0

CFP TFP 2009 and Functional Programming summer school: CEFP 2009
by Horváth Zoltán 19 Mar '09

19 Mar '09

Second call for papers 10th SYMPOSIUM ON TRENDS IN FUNCTIONAL PROGRAMMING TFP 2009 SELYE JANOS UNIVERSITY, KOMARNO, SLOVAKIA June 2-4, 2009 http://www.inf.elte.hu/tfp_cefp_2009 *** The registration and paper submission is now open! *** The symposium on Trends in Functional Programming (TFP) is an international forum for researchers with interests in all aspects of functional programming languages, focusing on providing a broad view of current and future trends in Functional Programming. It aspires to be a lively environment for presenting the latest research results. Acceptance for the conference is based on full papers or extended abstracts, and a formal post-symposium refereeing process selects the best articles presented at the symposium for publication in a high-profile volume. TFP 2009 is hosted by the Selye Janos University, Komarno, Slovakia, and it is co-located with the 3rd Central-European Functional Programming School (CEFP 2009), which is held immediately before TFP 2009 (May 25-30). IMPORTANT DATES (ALL 2009) * Paper Submission: March 31 (extended) * Notification of Acceptance: April 9 * Camera Ready Symposium Proceedings Paper: April 24 * TFP Symposium: June 2-4, 2009 * Post Symposium Paper Submission: June 30 * Notification of Acceptance: September 7 * Camera Ready Revised Paper: September 21 SCOPE OF THE SYMPOSIUM As part of the Symposium's focus on trends we therefore identify the following five article categories. High-quality articles are solicited in any of these categories: * Research: leading-edge, previously unpublished research. * Position: on what new trends should or should not be. * Project: descriptions of recently started new projects. * Evaluation: what lessons can be drawn from a finished project. * Overview: summarizing work with respect to a trendy subject. Articles must be original and not submitted for simultaneous publication to any other forum. They may consider any aspect of functional programming: theoretical, implementation-oriented, or more experience- oriented. Applications of functional programming techniques to other languages are also within the scope of the symposium. Contributions on the following subject areas are particularly welcomed: * Dependently Typed Functional Programming * Validation and Verification of Functional Programs * Debugging for Functional Languages * Functional Programming and Security * Functional Programming and Mobility * Functional Programming to Animate/Prototype/Implement Systems from Formal or Semi-Formal Specifications * Functional Languages for Telecommunications Applications * Functional Languages for Embedded Systems * Functional Programming Applied to Global Computing * Functional GRIDs * Functional Programming Ideas in Imperative or Object-Oriented Settings (and the converse) * Interoperability with Imperative Programming Languages * Novel Memory Management Techniques * Parallel/Concurrent Functional Languages * Program Transformation Techniques * Empirical Performance Studies * Abstract/Virtual Machines and Compilers for Functional Languages * New Implementation Strategies * Any new emerging trend in the functional programming area If you are in doubt on whether your article is within the scope of TFP, please contact the TFP 2009 program chairs, Zoltan Horvath and Viktoria Zsok at tfp2009(a)inf.elte.hu<mailto:tfp2009@inf.elte.hu> SUBMISSION AND DRAFT PROCEEDINGS Acceptance of articles for presentation at the symposium is based on the screening process of full papers (15 pages) and extended abstracts (at least 3 pages). TFP encourages PhD students to submit papers. PhD students may request the program committee to provide extensive feedback on their full papers at the time of submission. Full papers describing work accepted for presentation must be completed before the symposium for publication in the draft proceedings. Further details can be found at the TFP 2009 website. POST-SYMPOSIUM REFEREEING AND PUBLICATION In addition to the draft symposium proceedings, we continue the TFP tradition of publishing a high-quality subset of contributions in the Intellect series on Trends in Functional Programming. PROGRAM COMMITTEE * Peter Achten (symp-chair), Radboud University Nijmegen, NL * John Clements, California Polytechnic State University, USA * Cormac Flanagan, University of California at Santa Cruz, USA * Jurriaan Hage, Utrecht University, NL * Kevin Hammond, University of St. Andrews, UK * Michael Hanus, Christian-Albrechts University zu Kiel, DE * Ralf Hinze, University of Oxford, UK * Zoltan Horvath (PC co-chair), Eotvos Lorand University, HU * Graham Hutton, University of Nottingham, UK * Johan Jeuring, Utrecht University, NL * Pieter Koopman (symp-chair), Radboud University Nijmegen, NL * Hans-Wolfgang Loidl, Ludwig-Maximilians University Munchen, DE * Rita Loogen, Philipps-University Marburg, DE * Greg Michaelson, Heriot-Watt University, UK * Marco T. Morazan, Seton Hall University, USA * Rex L Page, University of Oklahoma, USA * Sven-Bodo Scholz, University of Hertfordshire, UK * Clara Segura, University Complutense de Madrid, ES * Mary Sheeran, Chalmers University of Technology, SE * Phil Trinder, Heriot-Watt University, UK * Marko van Eekelen, Radboud University Nijmegen, NL * Varmo Vene, University of Tartu, EE * Viktoria Zsok (PC co-chair), Eotvos Lorand University, HU LOCATION The Conference Centre of Selye University, Komarno, Slovakia (http://www.selyeuni.sk/) is a new and excellent conference centre with modern equipment, lecture rooms and computer labs. Komarno is on the north bank of river Danube, the northern part of the city Komarom / Komarno. It is a charming old city with about 30 000 inhabitants, 90 km away from Budapest (the capital of Hungary), with good highway and railway connections and 90 km away from Bratislava (the capital of Slovakia), about 100 km from Vienna International Airport. ----------- Call for participation 3rd CENTRAL EUROPEAN FUNCTIONAL PROGRAMMING SCHOOL CEFP 2009 SELYE JANOS UNIVERSITY, KOMARNO, SLOVAKIA May 25-30, 2009 http://www.inf.elte.hu/tfp_cefp_2009 *** The registration is now open! *** The Central European Functional Programming School (CEFP) is organised every second year (2005 Budapest - LNCS vol. 4164, 2007 Cluj-Napoca - LNCS vol. 5161, 2009 Komarno). It is the Central European counterpart of the Advanced Functional Programming school with the additional goal to stimulate students from Central Europe to attend. GOALS * Bring together computer scientists, in particular motivated graduate and PhD students, and make them familiar with the latest functional programming techniques. * Show the use of advanced functional programming techniques in real world applications. * Bridge the gap between recent results presented at programming conferences and material from introductory textbooks on functional programming. * Provide a forum for PhD students to present their research results as part of the workshop programme and submit the full paper version after the summer school. Selected and reviewed papers will be published in the LNCS Volume of the revised lectures. INVITED LECTURERS Our invited lecturers are top experts, professors and researchers from Europe and the US. * Francesco Cesarini: OTP Design Patterns (Erlang Training and Consulting Ltd, London, UK) Francesco Cesarini is owner and founder of Erlang Training and Consulting Ltd, a company specialised in high availability, massively concurrent soft real time systems. * Prof. Rinus Plasmeijer, Pieter Koopman: An effective methodology for defining consistent semantics of complex systems (Radboud University Nijmegen, The Netherlands) Rinus Plasmeijer is chief designer of the functional programming language Clean, member of IFIP WG 2.8., Head of Software Research Group, University Nijmegen, The Netherlands. Currently he is applying advanced functional programming techniques to enable model driven software development. He is working on the iTask system which enables the high-level specification of multi-user workflow systems for the web. Pieter Koopman's research is related to functional programming (especially the Clean language), and specification languages. Currently he is using Clean functions as specifications for the Generic Automatic Software Test-system (Gast). Earlier he was involved in project about parser combinators and implicit surfaces. * Matthew Fluet: Programming in Manticore, a heterogenous parallel language (Toyota Technological Institute at Chicago, USA) Matthew Fluet is active developer of MLton: an open-source, whole-program, optimizing Standard ML compiler. He is collaborating on the development of Manticore: a heterogeneous parallel programming language aimed at general-purpose applications running on multi-core processors. As a programming languages researcher, he is working on the opportunities for mechanizing reasoning about programming languages. * Prof. Ralf Hinze: Reasoning about codata (University of Oxford and Kellogg College, UK) Ralf Hinze's research centers around functional programming, particularly interested in functional algorithm design and purely functional data structures. At the moment he is mainly working on generic functional programming (Generic Haskell). In the past he worked on strictness analysis and type systems. * Prof. Mary Sheeran: Fun with combinators in Haskell (Chalmers University of Technology, Gothenburg, Sweden) Mary Sheeran's research interests are in functional programming, and particularly its application to designing and analysing hardware and hardware-like systems. She has worked on domain specific languages (DSLs) for hardware design (Lava, Wired) and is currently working with Ericsson and ELTE to develop a DSL for Digital Signal Processing. * Prof. John Hughes: QuickCheck, with a focus on industrial applications (http://quviq.com/) Research interests of John Hughes include type systems and formal semantics for programming languages, optimizing compilation, functional programming, and high-level language interoperability. He is currently working in the following projects: Combining Verification Methods in Software Development (Cover) and Flexible System-on-Chip Platforms for Embedded Applications (FlexSoC) * Andrew Kennedy: Advanced type systems for functional programming (Microsoft Research, Cambridge, England) Research interests of Andrew Kennedy include type systems and formal semantics for programming languages, optimizing compilation, functional programming, and high-level language interoperability. * Adam Granicz: Advanced F# Programming Adam Granicz is founder/CEO of Intellifactory Ltd. and he is a co-author of the Expert F# book. His research interests are formal environments and compilers, resource planning, and extensible compilers. PROGRAMME At the beginning of CEFP 2009 we make functional programming warm-up sessions starting on 21 May 2009. The summer school's programme includes: * In depth lectures about a selected number of recently emerged advanced functional programming techniques, taught by experts in the field. * Practical exercises accompanying the lectures to be solved by the students at the school. These exercises guide the students' learning to a great extent. A high quality lab is available at the school site. * Team work is stimulated, such that the students can also learn from each other. CEFP 2009 is co-located with the 10th Symposium on Trends in Functional Programming (TFP 2009, June 2-4), which is held after the summer school. LOCATION The Conference Centre of Selye University, Komarno, Slovakia (http://www.selyeuni.sk/) is a new and excellent conference centre with modern equipment, lecture rooms and computer labs. Komarno is on the north bank of river Danube, the northern part of the city Komarom / Komarno. It is a charming old city with about 30 000 inhabitants, 90 km away from Budapest (the capital of Hungary), with good motorway and railway connections and 90 km away from Bratislava (the capital of Slovakia), about 100 km from Vienna International Airport. ACCOMMODATION * hotels (from 30-66 Euro/night) * meals at the university canteen of the Conference Centre (included in the registration fee) LOCAL ARRANGEMENTS TEAM - CHAIR/CO-CHAIRS OC Chairs: * Zoltan Horvath * Viktoria Zsok (Eotvos Lorand University, Budapest) * Rinus Plasmeijer (Radboud University, Nijmegen) Local Co-chair of OC: * Veronika Stoffa, vice-rector (Selye Janos University, Komarno) Further details can be found at the CEFP website.

1 0

Google Summer of Code
by Malcolm Wallace 19 Mar '09

19 Mar '09

I am pleased to announce that haskell.org has once again been accepted as a mentoring organisation, for the 2009 Google Summer of Code. Student applications open on Monday (23rd March) at 1900 UTC, for a period of 12 days (until Fri 3rd April, also at 1900 UTC). Students applicants are encouraged to interact with the community via mailing lists, prior, during, and after the submission of their ideas for projects. In general terms, project ideas that benefit the whole community (e.g. infrastructure like ghc, cabal, libraries) will be preferred over things of more marginal interest (e.g. games). Unless you make a _really_ good case, of course! Because (sadly) the darcs community did not get accepted as a separate organisation this year, haskell.org will be willing to accept proposals relating to darcs (as it has done in previous years), but of course they will be competing in the general pool, alongside all the other ideas. Also, we are still accepting mentors. Regards, Malcolm

1 0

How do students learn Haskell? Postgraduate project at University of Kent
by S.J.Thompson 18 Mar '09

18 Mar '09

Funding is available for this postgraduate project, supervised by Simon Thompson and Sally Fincher, in collaboration with Jurriaan Hage, Utrecht University. To apply visit http://www.cs.kent.ac.uk/research/pg/ How do students learn Haskell? As users and teachers of Haskell, we have some sense of how people, both experienced programmers and novices, learn to program in Haskell. This sense is based on experience - as learners ourselves, perhaps, or through teaching. We propose an alternative approach, based on the wealth of data collected through the instrumented version of the Helium system for Haskell [1]. This collects information of the programs compiled, the errors they generate, and how learners use the system in fixing those errors, and so we can see precisely the way that learners use these tools while they are learning. This is a joint project of the Functional Programming and Computing Education groups at the University of Kent, and the Helium group at Utrecht. The CompEd group has experience of working on this sort of project [2], and the FP group has wide experience of teaching functional languages, particularly Haskell [3]. [1] Helium http://www.cs.uu.nl/wiki/Helium [2] ICER 2006 http://www.jadud.com/people/mcj/files/2006-icer-jadud.pdf [3] Craft http://www.cs.kent.ac.uk/people/staff/sjt/craft2e/

1 0

Re: indirectly recursive dictionaries
by oleg＠okmij.org 18 Mar '09

18 Mar '09

Tom Schrijvers wrote: > The cyclic dictionaries approach is a bit fragile. The problem appears to > be here that GHC alternates exhaustive phases of constraint reduction and > functional dependency improvement. The problem is that in your example you > need both for detecting a cycle. It seems we can convince GHC to do constraint reduction and improvement in the order we desire. The key is to use the continuation-passing style -- which forces things to happen in the right order, both at the run-time and at the compile time. I took the liberty to flesh out the example a bit more, to verify that recursive dictionaries are indeed constructed and used. The trace statement shows it. {-# OPTIONS -fglasgow-exts #-} {-# OPTIONS -fallow-overlapping-instances #-} {-# OPTIONS -fallow-undecidable-instances #-} import Debug.Trace class C1 x where m1 :: x -> Int instance (C1 x, C1 y) => C1 (x,y) where m1 (x,y) = m1 x + m1 y instance C1 Bool where m1 = fromEnum -- Was: instance (C2 x y, C1 (y,Bool)) => C1 x instance C2CPS x (C1K Bool) => C1 x where m1 x = trace "recursive C1" $ c2invoke (C1K True) x newtype C1K a = C1K a -- The class C2CPS below is a CPS version of the class C2 below -- class C2 x y | x -> y where c2 :: x -> y -- instance C2 Int Int where c2 = id -- The functional dependency becomes implicit class C2CPS x k where c2invoke :: k -> x -> Int instance Apply k Int Int => C2CPS Int k where c2invoke k x = apply k x class Apply f x y | f x -> y where apply:: f -> x -> y instance C1 (b,a) => Apply (C1K a) b Int where apply (C1K a) x = m1 (x,a) -- It is this declaration that was causing nontermination of typechecking. -- Not any more bar :: Int bar = m1 (1::Int)

1 0

Re: scoped type variables
by Norman Ramsey 18 Mar '09

18 Mar '09

[Opening discussion to broader audience: I asked Simon PJ about scoped type variables and type abbreviations] > | With scoped type variables, it would be useful to be able to define > | a type abbreviation in a where clause, so that the scoped > | type variable could be used on a right-hand side. Apparently > | this wasn't done. Was there any technical reason why not? > > Would you care to give an example? Do you mean > f x = e where a = Int No. I give an example below, but I've just spent 10 minutes grubbing through the Haskell 98 Report so I can phrase the question more precisely: Given the extension to scoped type variables, I believe that the 'type' abbreviation declaration should have been 'promoted' from syntactic category 'topdecl' to syntactic category 'decl', because it is convenient and useful to be able to exploit a scoped type variable in a type abbreviation. Was this possibility simply overlooked, or was a deliberate choice made not to do it? Here is a synopsis of code I would like to write: solve :: forall m l a . Graph m l -> Fuel -> DFM a (a, Fuel) solve = solveGraph where -- in the defintions below, type variable 'a' is free -- on the RHS but is bound by the forall above type FactKont b = Graph m l -> a -> Fuel -> DFM a b type FuelKont b = Graph m l -> Fuel -> DFM a b solveMid :: m -> FactKont b -> FactKont b solveLast :: l -> FuelKont b -> FactKont b ... For my sanity I'd like to define type abbreviations that refer to 'm' and 'l' also... Under the current regime, I'm forced to do what amounts to lambda lifting on the type abbreviations. Not only does this lead to a extra type parameters which distract from the main event, but in floating the type abbreviation out to top level, I am forced to choose a unique name for it, which I might prefer not to do if the same module contains several similar functions with similar (but not identical) type abbreviations. Of course the naming issue arises even in Haskell 98, but the ability to bring type variables into scope in a 'where' clause adds urgency. > There are lots of design issues. For example, in GHC today, a scoped type > variable stands for a type *variable* not for a *type*. I took the other > approach initially, but I think this is better I know this distinction is important in instance declarations. Presumably it also means that the scoped type variable can unify with something else during type inference? I fear that without seeing some formalism I can't be too sure what's going on---is there a technical report somewhere that explains the distinction? In any case, I hope this question is orthogonal to the problem of permitting a type declaration as a 'decl' in a where clause and not a mere lonely 'topdecl'. Is anybody else keen to have this ability? Norman

2 1

indirectly recursive dictionaries
by Ralf Laemmel 17 Mar '09

17 Mar '09

{- Recursive instance heads as in ... instance C0 (x,Bool) => C0 x ... are Ok if we allow for typechecking scheme as described in "SYB with class". The main idea is to assume C0 x in proving the preconditions of the body of the clause. This is also works for mutual recursion among type classes and instances to the extent exercised in ditto paper. What about the below example though? Here recursion detours through an extra class in a way that leads to nonterminating typechecking with GHC 6.10.1. Does anyone agree that a constraint resolution scheme like the one mentioned could be reasonably expected to cover this case? Regards, Ralf -} {-# OPTIONS -fglasgow-exts #-} {-# OPTIONS -fallow-overlapping-instances #-} {-# OPTIONS -fallow-undecidable-instances #-} -- Direct recursion terminates (typechecking-wise) class C0 x where m0 :: x -> () m0 = const undefined instance (C0 x, C0 y) => C0 (x,y) instance C0 Bool instance C0 (x,Bool) => C0 x foo :: () foo = m0 (1::Int) -- Indirect recursion does not terminate (typechecking-wise) class C1 x where m1 :: x -> () m1 = const undefined instance (C1 x, C1 y) => C1 (x,y) instance C1 Bool instance (C2 x y, C1 (y,Bool)) => C1 x class C2 x y | x -> y instance C2 Int Int -- It is this declaration that causes nontermination of typechecking. bar :: () bar = m1 (1::Int)

2 2

ANNOUNCE: libffi 0.1 released
by Remi Turk 17 Mar '09

17 Mar '09

I am happy to announce libffi 0.1, binding to the C library libffi, allowing C functions to be called whose types are not known before run-time. Why? Sometimes you can't use the haskell foreign function interface because you parse the type of the function from somewhere else, i.e. you're writing an interpreter for a language that has an FFI itself. What? The main function it exports is: callFFI :: FunPtr a -> RetType b -> [Arg] -> IO b And because code is worth a thousand words, here a small program that uses C to write a 1Gb buffer of random garbage to a file: > import System.Posix.DynamicLinker > import Foreign.LibFFI > > main = do > malloc <- dlsym Default "malloc" > creat <- dlsym Default "creat" > write <- dlsym Default "write" > let sz = 2 ^ 30 > buf <- callFFI malloc (retPtr retVoid) [argCSize sz] > fd <- callFFI creat retCInt [argString "/tmp/test", argCUInt 0o644] > n <- callFFI write retCSize [argCInt fd, argPtr buf, argCSize sz] > putStrLn $ show n ++ " bytes written" It should work on any 32/64bits machine on which libffi works, but has been primarily tested on linux x86_64. The current libffi is not exception-safe (exception = memory leak) and callFFI has quite some overhead that would be unnecessary with another api. It is, however, very easy to use :) More interesting examples are included in examples/ in the package. Where? Hackage: http://hackage.haskell.org/cgi-bin/hackage-scripts/package/libffi Module docs: http://www.science.uva.nl/~rturk/doc/libffi-0.1 Cheers, Remi

1 0

Re: indirectly recursive dictionaries
by oleg＠okmij.org 17 Mar '09

17 Mar '09

Ralf wrote: > class C1 x > where > m1 :: x -> () > m1 = const undefined > instance (C1 x, C1 y) => C1 (x,y) > instance C1 Bool > instance (C2 x y, C1 (y,Bool)) => C1 x > class C2 x y | x -> y > instance C2 Int Int > bar :: () > bar = m1 (1::Int) I believe it works very well (meaning bar typechecks and even runs) if we either add an instance instance C1 Int or change the instance of C2 to instance C2 Int Bool Otherwise, the problem really has no solution, and looping is an indication. I used GHC 6.8.3....

1 0