- Haskell - Haskell.org

Hackage download and popularity statistics
by Don Stewart 23 Mar '09

23 Mar '09

For the first time, we've got download and popularity statistics from Hackage: http://www.galois.com/blog/2009/03/23/one-million-haskell-downloads/ Find out if your package made the top 100, and when we reach our 1 millionth hackage download! -- Don

1 0

ANNOUNCE: WinGhci, a GUI for GHCI on Windows
by Pepe Gallardo 23 Mar '09

23 Mar '09

Hi, I am pleased to announce the first release of WinGhci. WinGhci is a simple GUI for GHCI on Windows. It is closely based on WinHugs, and provides similar functionality. WinGhci project web page: http://code.google.com/p/winghci/<mhtml:{5097F7F7-AA40-4661-A7CF-D5EEC38F084A}mid://00000003/!x-usc:http://co…> Binaries: http://winghci.googlecode.com/files/WinGhci-1.0-bin.zip<mhtml:{5097F7F7-AA40-4661-A7CF-D5EEC38F084A}mid://00000003/!x-usc:http://wi…> Sources: http://winghci.googlecode.com/files/WinGhci-1.0-src.zip<mhtml:{5097F7F7-AA40-4661-A7CF-D5EEC38F084A}mid://00000003/!x-usc:http://wi…> Acknowledgements Much of the code in WinGhci was taken from the Winhugs project. Many thanks to Neil Mitchell for giving us permission to use his code. <mhtml:{5097F7F7-AA40-4661-A7CF-D5EEC38F084A}mid://00000003/!x-usc:http://wi…> Pepe Gallardo

1 0

Cfp: WFLP09 - 18th Int'l Workshop on Functional and (Constraint) Logic Programming
by Santiago Escobar 23 Mar '09

23 Mar '09

******************************************************************* Call For Papers WFLP 2009 18th International Workshop on Functional and (Constraint) Logic Programming Brasilia, Brazil, June, 28, 2009 http://www.dsic.upv.es/workshops/wflp09/ ********* part of the Federated Conference on Rewriting, Deduction, and Programming RDP'09 http://rdp09.cic.unb.br/index.html ******************************************************************* IMPORTANT DATES Abstract Submission April 20, 2009 Full Paper Submission April 26, 2009 Acceptance Notification May 25, 2009 Preliminary Proceedings June 8, 2009 Workshop June 28, 2009 SCOPE The Workshop on Functional and (Constraint) Logic Programming aims at bringing together researchers interested in functional programming, (constraint) logic programming, as well as the integration of the two paradigms. It promotes the cross-fertilizing exchange of ideas and experiences among researchers and students from the different communities interested in the foundations, applications, and combinations of high-level, declarative programming languages and related areas. The previous WFLP editions are: WFLP 2008 (Siena, Italy), WFLP 2007 (Paris, France), WFLP 2006 (Madrid, Spain), WCFLP 2005 (Tallinn, Estonia), WFLP 2004 (Aachen, Germany), WFLP 2003 (Valencia, Spain), WFLP 2002 (Grado, Italy), WFLP 2001 (Kiel, Germany), WFLP 2000 (Benicassim, Spain), WFLP'99 (Grenoble, France), WFLP'98 (Bad Honnef, Germany), WFLP'97 (Schwarzenberg, Germany), WFLP'96 (Marburg, Germany), WFLP'95 (Schwarzenberg, Germany), WFLP'94 (Schwarzenberg, Germany), WFLP'93 (Rattenberg, Germany), and WFLP'92 (Karlsruhe, Germany). LOCATION WFLP'09 will be held in June 28, 2009 at Brasilia, Brazil, as part of the Federated Conference on Rewriting, Deduction, and Programming (RDP'09). WFLP'09 solicits papers in all areas of functional and (constraint) logic programming, including but not limited to: * Foundations: formal semantics, rewriting and narrowing, constraint solving, dynamics, type theory * Language Design: modules and type systems, multi-paradigm languages, concurrency and distribution, objects * Implementation: abstract machines, parallelism, compile-time and run-time optimizations, interfacing with external languages * Transformation and Analysis: abstract interpretation, specialization, partial evaluation, program transformation, meta-programming * Software Engineering: design patterns, specification, verification and validation, debugging, test generation * Integration of Paradigms: integration of declarative programming with other paradigms such as imperative, object-oriented, concurrent, and real-time programming * Applications: security, declarative programming in education and industry, domain-specific languages, visual/graphical user interfaces, embedded systems, WWW applications, knowledge representation and machine learning, deductive databases, advanced programming environments and tools SUBMISSIONS and PROCEEDINGS Authors are invited to submit papers of at most 15 pages (pdf or postscript formats) presenting original, not previously published works. Submission categories include regular research papers, short papers (not more than 8 pages) describing on-going work, and system descriptions. Submissions must be formatted in the Lecture Notes in Computer Science style (excluding well-marked appendices not intended for publication). Papers should be submitted electronically via the web-based submission site http://www.easychair.org/conferences/?conf=wflp2009 Preliminary proceedings will be available at the workshop. Selected authors will be invited to submit a full version of their papers after the workshop. Contributions accepted for the post-workshop proceedings will be published in Lecture Notes in Computer Science. INVITED SPEAKERS Claude Kirchner INRIA Bordeaux - Sud-Ouest, France Roberto Ierusalimschy Departamento de Informatica, PUC-Rio, Brazil PROGRAM CHAIR Santiago Escobar Universidad Politecnica de Valencia, Spain PROGRAM COMMITTEE Maria Alpuente Universidad Politecnica de Valencia, Spain Sergio Antoy Portland State University, USA Christiano Braga Universidade Federal Fluminense, Brazil Rafael Caballero Universidad Complutense de Madrid, Spain David Deharbe Universidade Federal do Rio Grande do Norte, Brazil Rachid Echahed CNRS,laboratoire LIG, France Moreno Falaschi Universita di Siena, Italy Michael Hanus Christian-Albrechts-Universitaet zu Kiel, Germany Frank Huch Christian-Albrechts-Universitaet zu Kiel, Germany Tetsuo Ida University of Tsukuba, Japan Wolfgang Lux Westfalische Wilhelms-Universitat Munster, Germany Mircea Marin University of Tsukuba, Japan Camilo Rueda Universidad Javeriana-Cali, Colombia Jaime Sanchez-Hernandez Universidad Complutense de Madrid, Spain Anderson Santana de Oliveira Universidade Federal do Rio Grande do Norte, Brazil

1 0

[ANN] ansi-terminal, ansi-wl-pprint - ANSI terminal support for Haskell
by Max Bolingbroke 21 Mar '09

21 Mar '09

These two packages allow Haskell programs to produce much richer console output by allowing colorisation, emboldening and so on. Both Unix-like (OS X, Linux) and Windows operating systems are supported (via a pure Haskell ANSI emulation layer for Windows). Examples, screenshots, and lots more information about how to get the packages are available at the freshly-minted homepages: http://batterseapower.github.com/ansi-terminal/ http://batterseapower.github.com/ansi-wl-pprint/ These two packages have actually been in stealth release mode on Hackage for some time. However, they seem to be getting some use and I'm not getting any bug reports, so I figure that they /must/ be stable enough to make a proper announcement :-) Cheers, Max (p.s: the GitHub "pages" feature seems to be absolutely ace - highly reccomended! http://pages.github.com/)

2 1

Haskell Weekly News: Issue 110 - March 21, 2009
by Brent Yorgey 21 Mar '09

21 Mar '09

--------------------------------------------------------------------------- Haskell Weekly News http://sequence.complete.org/hwn/20090321 Issue 110 - March 21, 2009 --------------------------------------------------------------------------- Welcome to issue 110 of HWN, a newsletter covering developments in the [1]Haskell community. [2]Facebook apps with Happstack, [3]Sudoku with Cryptol, what next? Tic-tac-toe with darcs? Anyway, lots of neat stuff this week, including new releases of [4]GHC, [5]jhc, and the [6]Monad.Reader, some [7]fun [8]visualizations, and more. Also, students: apply to work on a [9]Haskell project for the Google Summer of Code! Announcements GHC 6.10.2 Release Candidate 1. Ian Lynagh [10]announced the [11]first release candidate for GHC 6.10.2. Please test as much as possible; bugs are much cheaper if we find them before the release! jhc 0.6.0 Haskell Compiler. John Meacham [12]announced the release of [13]jhc 0.6.0. Safe Lazy IO in Haskell. Nicolas Pouillard [14]announced the [15]safe-lazy-io package that provides special types and combinators for performing safe lazy I/O. game-tree - a library for searching game trees. Colin Paul Adams [16]announced [17]game-tree 0.1.0.0, which provides a class for dynamic game trees, and purely functional algorithms for searching them. random-shuffle package. Manlio Perillo [18]announced the availability of the [19]random-shuffle package, which is based on [20]Oleg's description. random-stream package. Manlio Perillo [21]announced the [22]random-stream package, which provides a portable interface for the operating system source of pseudo random data. Supported sources are Unix /dev/urandom, Win32 CryptGenRandom and OpenSSL pseudo random numbers generator. language-python. Bernie Pope [23]announced the [24]language-python package, which provides a parser (and lexer) for Python, written in Haskell. Currently it only supports version 3 of Python (the most recent version), but it will support version 2 in the future. Google Summer of Code. Malcolm Wallace [25]announced 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. 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. regex-tdfa-1.1.0. ChrisK [26]announced the release of [27]regex-tdfa-1.1.0. This version is a small performance update to the old regex-tdfa-1.0.0 version. Previously all text (e.g. ByteString) being search was converted to String and sent through a single engine; the new version uses a type class and SPECIALIZE pragmas to avoid converting to String. This should make adding support for searching other Char containers easy to do. Haskell on your system? Information wanted!. Don Stewart [28]announced that haskell.org now features links to wiki pages explaining how to obtain Haskell on windows, mac osx and linux and bsd. If you're a distro maintainer for these systems, please consider adding relevant pointers to the pages, so that users of these systems can find all the info they need. libffi 0.1 released. Remi Turk [29]announced the release of [30]libffi 0.1, bindings to the C library libffi, allowing C functions to be called whose types are not known before run-time. Haskell Logo Voting has started!. Eelco Lempsink [31]announced that voting has begun to choose the new Haskell logo. All subscribed to haskell-cafe should have received a ballot; if you are not directly subscribed, you can still send ballot requests until the end of the competition (March 24, 12:00 UTC). Make sure the message contains 'haskell logo voting ballot request' in the subject. A long discussion of what color to paint the bike shed and why this particular bike shed will not do for storing bikes ensued. The Monad.Reader (13). Wouter Swierstra [32]announced that a new issue of [33]The Monad.Reader, a quarterly magazine about functional programming, is now available. Issue 13 consists of the following four articles: "Rapid Prototyping in TEX" by Stephen Hicks; "The Typeclassopedia" by Brent Yorgey; a Real World Haskell book review by Chris Eidhof and Eelco Lempsink; and "Calculating Monads with Category Theory" by Derek Elkins. dzen-utils 0.1. Felipe Lessa [34]announced the release of [35]dzen-utils 0.1, which contains various utilities for creating dzen input strings in a type-safe way using some combinators, including the ability to apply colors locally (instead of applying for everything beyond some point). It can also emulate dbar and gdbar, do automatic padding, and more. Discussion transformers versus mtl. Ganesh Sittampalam began a [36]discussion on the relative status of the 'transformers' and 'mtl' packages. least fixed points above something. Jens Blanck [37]asked about a function to compute fixed points starting from a seed value (as opposed to computing the least defined fixed point). Type equality proof. Martijn van Steenbergen [38]requested feedback on a proposed module collecting utilities for working with type equality proofs. What unsafeInterleaveIO is unsafe. Yusaku Hashimoto began a [39]discussion by asking why unsafeInterleaveIO is considered unsafe, or under what circumstances its use can be considered safe. Jobs How do students learn Haskell? Postgraduate project at University of Kent. S.J.Thompson [40]announced that funding is available for a [41]postgraduate project to study how students learn Haskell, based on the wealth of data collected through the instrumented version of the [42]Helium system for Haskell. The project will be supervised by Simon Thompson and Sally Fincher, in collaboration with Jurriaan Hage, Utrecht University. Blog noise [43]Haskell news from the [44]blogosphere. * Neil Mitchell: [45]Concise Generic Queries. Neil compares solving a query problem with several different generic programming libraries. * Jeff Heard: [46]Preview: Data Waves. A neat new type of data visualization, built using Hieroglyph. * >>> necrobious: [47]A fun example of Haskell's newtype. * GHC / OpenSPARC Project: [48]Peak issue rate is 18.64 Gig instrs/sec. * happstack.com: [49]Jeremy Shaw creates first Facebook App with Happstack. * GHC / OpenSPARC Project: [50]Peak performance. * Galois, Inc: [51]Solving Sudoku Using Cryptol. * Xmonad: [52]xmonad on ubuntu. A tutorial on getting started with xmonad on Ubuntu. * Don Stewart (dons): [53]Visualising the Haskell Universe. Pretty dependency graphs of ten thousand Haskell modules! * >>> Sean Chapel: [54]Haskell. * >>> Dean Berris: [55]The Haskell Experiment: HaskellDB, HTTP, and Monads. * Holumbus: [56]Hayoo! Update. The Hayoo! package index has been updated to include everything currently on Hackage! * >>> John Wiegley: [57]Journey into Haskell, Part 1. John ventures down the rabbit hole. * Bjorn Buckwalter: [58]Blogging with Pandoc, literate Haskell, and a bug. * Bjorn Buckwalter: [59]Extended sessions with the Haskell Curl bindings. * Brent Yorgey: [60]Monad.Reader #13 is out!. * Manuel M T Chakravarty: [61]Final version of "GPU Kernels as Data-Parallel Array Computations in Haskell".. * Xmonad: [62]Visualising xmonad. * Darcs: [63]darcs weekly news #21. * mightybyte: [64]Transactional Integrity Problem. * >>> Dean Berris: [65]The Haskell Experiment: Learning a New Programming Language. * >>> John Wiegley: [66]Hello Haskell, Goodbye Lisp. Quotes of the Week * ray: three dimensional zippers make my scalp hurt when i get my hair caught in them * dolio: [regarding a paypal spam message on #haskell] Take that, Harrop! Does OCaml have illegal cracking utilities? * lament: I think I speak for everyone in this channel when I say haskell is absolutely horrible and nobody would ever want to use it * MiguelMitrofanov: The first glimpse of this [logo] vote scared me so much that I've closed the page, stopped the browser, and shut my computer down. * osfameron: <ImInYourMonad> can I store gtk2hs-Buttons in a datastructure? <osfameron> ImInYourMonad: I think you have to sew them on with gtk2hs-Thread * chrisdone: I think you mean Peyton `Simon` Jones. About the Haskell Weekly News New editions are posted to [67]the Haskell mailing list as well as to [68]the Haskell Sequence and [69]Planet Haskell. [70]RSS is also available, and headlines appear on [71]haskell.org. To help create new editions of this newsletter, please see the information on [72]how to contribute. Send stories to byorgey at cis dot upenn dot edu. The darcs repository is available at darcs get [73]http://code.haskell.org/~byorgey/code/hwn/ . References 1. http://haskell.org/ 2. http://blog.happstack.com/2009/03/18/jeremy-shaw-creates-first-facebook-app… 3. http://www.galois.com/blog/2009/03/18/solving-sudoku-using-cryptol/ 4. http://article.gmane.org/gmane.comp.lang.haskell.glasgow.user/16506 5. http://www.haskell.org//pipermail/haskell/2009-March/021116.html 6. http://www.haskell.org/haskellwiki/The_Monad.Reader 7. http://vis.renci.org/jeff/2009/03/20/preview-data-waves/ 8. http://donsbot.wordpress.com/2009/03/16/visualising-the-haskell-universe/ 9. http://article.gmane.org/gmane.comp.lang.haskell.cafe/55109 10. http://article.gmane.org/gmane.comp.lang.haskell.glasgow.user/16506 11. http://www.haskell.org/ghc/dist/6.10.2-rc1/ 12. http://www.haskell.org//pipermail/haskell/2009-March/021116.html 13. http://repetae.net/computer/jhc/ 14. http://article.gmane.org/gmane.comp.lang.haskell.general/16977 15. http://hackage.haskell.org/cgi-bin/hackage-scripts/package/safe%2Dlazy%2Dio 16. http://article.gmane.org/gmane.comp.lang.haskell.general/16976 17. http://hackage.haskell.org/cgi-bin/hackage-scripts/package/game%2Dtree 18. http://article.gmane.org/gmane.comp.lang.haskell.cafe/55159 19. http://haskell.mperillo.ath.cx/random-shuffle-0.0.2.tar.gz 20. http://okmij.org/ftp/Haskell/perfect-shuffle.txt 21. http://article.gmane.org/gmane.comp.lang.haskell.cafe/55143 22. http://haskell.mperillo.ath.cx/random-stream-0.0.1.tar.gz 23. http://article.gmane.org/gmane.comp.lang.haskell.cafe/55116 24. http://projects.haskell.org/language-python/ 25. http://article.gmane.org/gmane.comp.lang.haskell.cafe/55109 26. http://article.gmane.org/gmane.comp.lang.haskell.cafe/55073 27. http://hackage.haskell.org/cgi-bin/hackage-scripts/package/regex%2Dtdfa 28. http://article.gmane.org/gmane.comp.lang.haskell.cafe/55036 29. http://article.gmane.org/gmane.comp.lang.haskell.cafe/54959 30. http://hackage.haskell.org/cgi-bin/hackage-scripts/package/libffi 31. http://article.gmane.org/gmane.comp.lang.haskell.cafe/54958 32. http://article.gmane.org/gmane.comp.lang.haskell.cafe/54880 33. http://www.haskell.org/haskellwiki/The_Monad.Reader 34. http://article.gmane.org/gmane.comp.lang.haskell.cafe/54835 35. http://hackage.haskell.org/cgi-bin/hackage-scripts/package/dzen-utils 36. http://thread.gmane.org/gmane.comp.lang.haskell.libraries/10807 37. http://thread.gmane.org/gmane.comp.lang.haskell.cafe/55132 38. http://thread.gmane.org/gmane.comp.lang.haskell.cafe/54946 39. http://thread.gmane.org/gmane.comp.lang.haskell.cafe/54840 40. http://article.gmane.org/gmane.comp.lang.haskell.general/16967 41. http://www.cs.kent.ac.uk/research/pg/ 42. http://www.cs.uu.nl/wiki/Helium 43. http://planet.haskell.org/ 44. http://haskell.org/haskellwiki/Blog_articles 45. http://neilmitchell.blogspot.com/2009/03/concise-generic-queries.html 46. http://vis.renci.org/jeff/2009/03/20/preview-data-waves/ 47. http://necrobious.blogspot.com/2009/03/fun-example-of-haskells-newtype.html 48. http://ghcsparc.blogspot.com/2009/03/peak-issue-rate-is-1864-gig-instrssec.… 49. http://blog.happstack.com/2009/03/18/jeremy-shaw-creates-first-facebook-app… 50. http://ghcsparc.blogspot.com/2009/03/peak-performance.html 51. http://www.galois.com/blog/2009/03/18/solving-sudoku-using-cryptol/ 52. http://xmonad.wordpress.com/2009/03/18/xmonad-on-ubuntu/ 53. http://donsbot.wordpress.com/2009/03/16/visualising-the-haskell-universe/ 54. http://seanchapel.blogspot.com/2009/03/haskell.html 55. http://www.deanberris.com/mental-blabberings/2009/3/17/the-haskell-experime… 56. http://holumbus.fh-wedel.de/blog/?p=19 57. http://www.newartisans.com/2009/03/journey-into-haskell-part-1.html 58. http://flygdynamikern.blogspot.com/2009/03/blogging-with-pandoc-literate-ha… 59. http://flygdynamikern.blogspot.com/2009/03/extended-sessions-with-haskell-c… 60. http://byorgey.wordpress.com/2009/03/16/monadreader-13-is-out/ 61. http://justtesting.org/post/86905420 62. http://xmonad.wordpress.com/2009/03/16/visualising-xmonad/ 63. http://blog.darcs.net/2009/03/darcs-weekly-news-21.html 64. http://softwaresimply.blogspot.com/2008/02/transactional-integrity-problem.… 65. http://www.deanberris.com/mental-blabberings/2009/3/14/the-haskell-experime… 66. http://www.newartisans.com/2009/03/hello-haskell-goodbye-lisp.html 67. http://www.haskell.org/mailman/listinfo/haskell 68. http://sequence.complete.org/ 69. http://planet.haskell.org/ 70. http://sequence.complete.org/node/feed 71. http://haskell.org/ 72. http://haskell.org/haskellwiki/HWN 73. http://code.haskell.org/~byorgey/code/hwn/

1 0

Call For Papers: SBLP 2009
by Andre Rauber Du Bois 21 Mar '09

21 Mar '09

13th BRAZILIAN SYMPOSIUM ON PROGRAMMING LANGUAGES http://sblp2009.ucpel.tche.br Gramado, Rio Grande do Sul, Brazil August 19-21, 2009 Abstract Submission: April, 6 Paper Submission: April, 13 SBLP is a *Qualis A* Brazilian Conference CALL FOR PAPERS AND TUTORIALS The 13th Brazilian Symposium on Programming Languages, SBLP 2009, will be held in Gramado, Rio Grande do Sul, Brazil, on August 19-21, 2008. SBLP provides a venue for researchers and practitioners interested in the fundamental principles and innovations in the design and implementation of programming languages and systems. This year the symposium will be co-located with the Brazilian Symposium on Formal Methods, which will happen in the same week and in the same venue. SBLP 2009 invites authors to contribute with Technical Papers and Tutorial Proposals related (but not limited) to: * Programming language design and implementation * Formal semantics of programming languages * Theoretical foundations of programming languages * Design and implementation of programming language environments * Object-oriented programming languages * Functional programming * Aspect-oriented programming languages * Scripting languages * Domain-specific languages * Programming languages for mobile, web and network computing * New programming models * Program transformations * Program analysis and verification * Compilation and interpretation techniques Contributions can be written in Portuguese or English. Papers should have at most 14 pages. All accepted papers will be published in the conference proceedings. Selected papers written in English should be invited for a journal publication. Papers should be presented in the language of submission. Tutorial submissions must be in the form of an extended abstract with at most 10 pages. The final version of accepted tutorials should contain at most 30 pages. This final version will be distributed to attendees. An abstract of the tutorial (1-2 pages) will be included in the conference proceedings. Detailed submission guidelines will be available at http://sblp2009.ucpel.tche.br IMPORTANT DATES Paper abstract submission (15 lines): April 6, 2009 Full paper submission: April 13, 2009 Notification of acceptance: June 8, 2009 Final papers due: June 30, 2009 BEST PAPER AWARD Awards will be given for the best papers at the symposium. GENERAL CHAIR Andre Rauber Du Bois, UCPel PROGRAMME CHAIRS Andre Santos, UFPE, Brazil Joao Saraiva, Universidade do Minho, Portugal PROGRAMME COMMITTEE Alberto Pardo, Univ. de La Republica Alex Garcia, IME Alfio Martini, PUC-RS Alvaro Freitas Moreira, UFRGS Andre Rauber Du Bois, UCPel Carlos Camarao, UFMG Christiano Braga, Univ. Comp. de Madrid Cristiano Damiani, UFPEL Edward Hermann Haeusler, PUC-Rio Eric Tanter, Univ. of Chile Fernando Castor Filho, UFPE Francisco Heron de Carvalho Junior, UFC Isabel Cafezeiro, UFF Johan Jeuring, Utrecht Univ. Jose Guimaraes, UFSCAR Jose E. Labra Gayo, Univ. of Oviedo Jose Luiz Fiadeiro, Univ. of Leicester Lucilia Figueiredo, UFOP Luis Soares Barbosa, Univ. do Minho Luis Carlos Meneses, UPE Marcelo A. Maia, UFU Marco Tulio Valente, PUC Minas Mariza A. S. Bigonha, UFMG Martin A. Musicante, UFRN Noemi Rodriguez, PUC-Rio Paulo Borba, UFPE Peter Mosses, Swansea University Rafael Dueire Lins, UFPE Renato Cerqueira, PUC-Rio Ricardo Massa Lima, UFPE Roberto S. Bigonha, UFMG Roberto Ierusalimschy, PUC-Rio Rodolfo Jardim de Azevedo, UNICAMP Sandro Rigo, UNICAMP Sergio de Mello Schneider, UFU Sergio Soares, UFRPE Sergiu Dascalu, Univ. of Nevada Simon Thompson, Univ. of Kent Varmo Vene, Univ. de Tartu Vladimir Di Iorio, UFV Vitor Santos Costa, UFRJ ORGANIZATION Brazilian Computer Society and Universidade Catolica de Pelotas

1 0

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 18 Mar '09

18 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