April 2010 - Haskell - Haskell.org

VSTTE 2010: Call for POSTERS
by Gudmund Grov 26 Apr '10

26 Apr '10

(* Apologies if you receive multiple copies of this announcement *) ***************************************************************** *** Call for POSTERS *** 3rd International Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2010) Edinburgh, Scotland August 16th-19th, 2010 http://www.macs.hw.ac.uk/vstte10 POSTER SESSION The complementary themes of Theories, Tools and Experiments makes VSTTE an unique conference. Through the introduction of a POSTER session at VSTTE 2010, we are aiming to widen the body of researchers that are involved in the Verified Software Initiative (VSI) and its related Challenges (more details on VSTTE & VSI are provided below). Limited financial support will be available if necessary to enable attendance of both MSc and PhD students whose posters are accepted. Specifically, we aim to attract students who are already engaged in theories or tools or experiments relevant to verification; and give them an opportunity to meet other students and researchers engaged in complementary experiments or theories or tools. Note that the POSTER session is open to all researchers, not just students. With regards to submissions, we require the following: 1. 1-page abstract of your research 2. Poster OR a poster plan 3. For students, a supporting statement from your supervisor Submissions should be sent electronically to vstte10(a)macs.hw.ac.uk. The timetable for POSTER authors is as follows: JUNE 18: Submission of abstract & poster (plan) deadline JUNE 30: Notification of decision JULY 31: Camera-ready abstract deadline AUGUST 17: Poster session Note that a collection of abstracts for the accepted posters will be distributed at the conference. Poster authors will be expected to bring their poster with them to the conference. Details of the size of the final posters will be provided in due course. Financial support will be allocated on a case-by-case basis, and will support around 30 partial/fully funded places, including 10 SICSA PhD funded places. If you have any queries, please direct them to vstte10(a)macs.hw.ac.uk MORE DETAILS ON VSTTE 2010 SPONSORS National Science Foundation (NSF) Engineering and Physical Sciences Research Council (EPSRC) Microsoft Research Scottish Informatics & Computer Science Alliance (SICSA) Altran Praxis Software Systems Engineering Initiative (SSEI) Formal Methods Europe (FME) WHAT IS THE HISTORY OF VSTTE? The Third International Conference on Verified Software: Theories, Tools, and Experiments follows a successful inaugural working conference at Zurich (2005) and a successful conference in Toronto (2008). This conference is part of the Verified Software Initiative (VSI), a fifteen-year, cooperative, international project directed at the scientific challenges of large-scale software verification. VSI also includes UKCRC's Grand Challenge 6, i.e. Dependable Systems Evolution. VSTTE is open to anyone who is interested in participating actively in the VSI effort. SCOPE The goal of this conference is to advance the state of the art in the science and technology of software verification through the interaction of theory development, tool evolution, and experimental validation. Authors are encouraged to submit work in progress, particularly if the work involves collaboration, theory unification, and tool integration. Topics of interest include requirements modeling specification languages specification/verification case-studies formal calculi programming languages language semantics software design methods software testing automatic code generation refinement methodologies type systems computer security verification tools (static analysis, dynamic analysis, model checking, theorem proving, satisfiability) tool integration benchmarks challenge problems integrated verification environments We also encourage researchers to submit challenges in theory, formalization, systems verification, code verification, and applications. Contributions relating to existing challenges will also be welcomed, i.e. * POPLMark (http://tinyurl.com/poplmark) * Tokeneer (http://www.adacore.com/home/products/sparkpro/tokeneer) * POSIX file system (http://tinyurl.com/qyzqk9) * medical devices (http://tinyurl.com/pnztqb) VENUE VSTTE 2010 is being hosted by Heriot-Watt University in Edinburgh. The conference dates coincide with the 2010 Edinburgh International Festival and the Edinburgh Festival Fringe -- collectively the largest annual arts festival on the planet! The technical programme will take place in the Edinburgh Conference Centre (Riccarton campus), where accommodation will be available at very competitive rates for festival time. Social events will be arranged within the city centre, making VSTTE an unique cultural and scholarly event for 2010! INVITED SPEAKERS * Tom Ball (Microsoft Research, Redmond) * Gerwin Klein (National ICT Australia) * Matthew Parkinson (University of Cambridge) WORKSHOPS In addition to the main conference, VSTTE will host two workshops on August 19th: * VS-Theory focuses on theoretical foundations of software verification. Topics range from the difficult and essential study of soundness of delicate proof methods, to the discovery of new specification techniques and proof methods, to dramatic simplification or unification of existing methods, to as yet unknown breakthroughs. * VS-Tools & Experiments focuses on the development of verification tools and their experimental evaluation. Possible topics include interfaces between tools, tool integration platforms, and case studies. The workshops will provide a forum to present new, possibly unfinished work and will also give the opportunity to propose research challenges, which will help form a research agenda for the Verified Software Initiative. Papers must be written in English using Springer LNCS style. The page limit is 10 pages for technical papers and 5 pages for proposals of verification challenges. The proceedings will be published as a technical report. SUMMER SCHOOL There will be a two-day summer-school preceding the main conference on the 14 and 15 August. The summer school will give a broad overview of software verification techniques, addressing both bottom-up and top-down approaches with a strong focus on the formal representation and reasoning themes. The school consists of eight introductory lectures, each concentrating on an unique aspect of one or both of the overall themes. The topics of the lectures include inductive theorem proving; SAT and SMT solving; proof planning and rippling; rely/guarantee conditions; separation logic; operating system verification; formal analysis of security. The following will present at the summer school: * Robert Atkey (University of Strathclyde) & Ewen Maclean (Heriot-Watt University) * Alan Bundy & Lucas Dixon (University of Edinburgh) * Cliff Jones (University of Newcastle) * Gerwin Klein (National ICT Australia) * J Strother Moore (University of Texas at Austin) * Natarajan Shankar (SRI) * Graham Steel (INRIA) The school is intended for PhD students and researchers working within one or both of these themes, however familiarity with any of the techniques is not a prerequisite. All lectures are meant to be introductory. For more information see: http://dream.inf.ed.ac.uk/events/ssfrr-2010/ COMPETITION A verification competition will be held at VSTTE 2010. The challenge is to develop a machine-verified piece of software with respect to a given specification. The competition will be conducted over a 2.5 hour period on some evening of the conference. The problem will be presented with a logical specification and test cases over .5 hours including time for discussion with 2 hours to construct a solution. Each competing team can feature up to three members. You can use any tool or combination of tools as well as libraries, but you cannot modify these tools. You can reinterpret the specification to suit your tools and methods, but you will be judged on the fidelity of your interpretation. The goal is to produce an executable program and a replayable proof that the program meets the specification. It will be possible to code the solution using integers and arrays. The solutions will be judged for soundness (absence of bugs) and completeness (presence of proofs). The three best solutions will be selected and the respective teams will be invited to make presentations at the tools/experiments workshop. You must register a copy of the verification system with the judges prior to the competition with instructions for replaying proofs and running the programs. CONFERENCE CHAIR Andrew Ireland (Heriot-Watt University; A.Ireland(a)hw.ac.uk) PROGRAM CHAIRS Peter O'Hearn (Queen Mary, University of London; ohearn(a)dcs.qmul.ac.uk) Gary T. Leavens (University of Central Florida; leavens(a)eecs.ucf.edu) Sriram Rajamani (Microsoft Research; sriram(a)microsoft.com) WORKSHOP GENERAL CHAIR Peter Mueller (ETH Zurich; peter.mueller(a)inf.ethz.ch) THEORY WORKSHOP CHAIRS David Naumann (Stevens Institute of Technology; dnaumann(a)stevens.edu) Hongseok Yang (Queen Mary, University of London; hyang(a)dcs.qmul.ac.uk) TOOLS & EXPERIMENTS WORKSHOP CHAIRS Rajeev Joshi (NASA JPL; rajeev.joshi(a)jpl.nasa.gov) Tiziana Margaria (Universitat Potsdam; margaria(a)cs.uni-potsdam.de) PUBLICITY CHAIR Gudmund Grov (Edinburgh University; ggrov(a)inf.ed.ac.uk) LOCAL ARRANGEMENT CHAIR Ewen Maclean (Heriot-Watt University; E.A.H.Maclean(a)hw.ac.uk) CONFERENCE PROGRAM COMMITTEE Ahmed Bouajjani Leo Freitas Philippa Gardner John Hatcliff Ranjit Jhala Joseph Kiniry Rustan Leino Xavier Leroy David Naumann Matthew Parkinson Wolfgang Paul Shaz Qadeer Andrey Rybalchenko Augusto Sampaio Zhong Shao Aaron Stump Serdar Tasiran Willem Visser Chin Wei-Ngan Stephanie Weirich Greta Yorsh STEERING COMMITTEE Tony Hoare Jay Misra Natarajan Shankar Jim Woodcock -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.

1 0

ANN: hstatistics 0.1.0.1
by Alexander McPhail 21 Apr '10

21 Apr '10

Dear All, hstatistics is a purely functional statistics package which has wrappers to the GSL statistics functions and is based on Alberto Ruiz's hmatrix package. Cheers.

1 0

Philadelphia Haskell hackathon -- reduced hotel rate ends Friday April 23!
by Brent Yorgey 21 Apr '10

21 Apr '10

There is still plenty of space to register [1] for Hac phi 2010, but time is running out to get a hotel room at a reduced rate --- if you want the special rate for the block of rooms we have reserved at the Club Quarters, you must contact the hotel by this Friday, April 23. Instructions are on the wiki [2]. If you have been thinking of coming but are not sure, let me emphasize that last year's Hac phi was great fun---it will be an excellent time to make new friends, expand your brain, eat good food, and of course write some Haskell. You are welcome and encouraged to attend whether you just want to learn Haskell or have been using it for 10 years! You also do not have to come for the whole time; feel free to come just for a day or even an afternoon. The original announcement is below. -Brent ---------- Hac phi 2010 is a Haskell hackathon/get-together to be held May 21-23 at the University of Pennsylvania in Philadelphia. The hackathon will officially kick off at 2:30 Friday afternoon, and go until 5pm on Sunday (with breaks for sleep, of course). Last year's Hac phi was a lot of fun, and many people have already expressed interest in coming back this year. I want to stress that everyone is welcome---you do not have to be a Haskell guru to attend! Helping hack on someone else's project could be a great way to increase your Haskell-fu. If you plan on coming, please officially register [1]. Registration, travel, lodging and many other details can be found on the Hac phi wiki [2]. Note that we're in a different space this year and may have to cap attendance, so register early. We're also looking for a few people interested in giving short (15-20 min.) talks, probably on Saturday afternoon. Anything of interest to the Haskell community is fair game---a project you've been working on, a paper, a quick tutorial. If you'd like to give a talk, add it on the wiki [3]. Hope to see you in Philadelphia! -The Hac φ team [1] http://haskell.org/haskellwiki/Hac_φ/Register [2] http://haskell.org/haskellwiki/Hac_φ [3] http://haskell.org/haskellwiki/Hac_φ/Talks

1 0

ANN: forkable-monad 0.1
by David Anderson 20 Apr '10

20 Apr '10

Dear Haskellers, I'm happy, and only slightly intimidated, to announce the initial release of forkable-monad. The short version is that forkable-monad exports a replacement forkIO that lets you do this: type MyMonad = ReaderT Config (StateT Ctx IO) startThread :: MyMonad ThreadId startThread = forkIO threadMain threadMain :: MyMonad () threadMain = forever $ liftIO $ putStrLn "Painless monad stack forking!" Note the lack of monad stack deconstruction and reconstruction to transport it over to the new thread. You'll find the details in the Haddock documentation for the module. forkable-monad is available: * On hackage: http://hackage.haskell.org/package/forkable-monad * Via cabal: cabal install forkable-monad * Source and issue tracker: http://code.google.com/p/forkable-monad/ Feedback is of course welcome. As this is my first published Haskell code and Hackage upload, I expect there will be quite a bit! - Dave

1 0

CFT: Haskell Implementors' Workshop 2010 (co-located with ICFP)
by Simon Marlow 19 Apr '10

19 Apr '10

Call for Talks ACM SIGPLAN Haskell Implementors' Workshop http://haskell.org/haskellwiki/HaskellImplementorsWorkshop/2010 Baltimore, Maryland, USA, October 1, 2010 The workshop will be held in conjunction with ICFP 2010 http://www.icfpconference.org/icfp2010/ Important dates Proposal Deadline: 6 August 2010 Notification: 23 August 2010 The Haskell Implementors' Workshop is a workshop to be held alongside ICFP 2010 this year in Baltimore, Maryland, USA. There will be no proceedings; it is an informal gathering of people involved in the design and development of Haskell implementations, tools, libraries, and supporting infrastructure. This relatively new workshop reflects the growth of the user community: there is a clear need for a well-supported tool chain for the development, distribution, deployment, and configuration of Haskell software. The aim is for this workshop to give the people involved with building the infrastructure behind this ecosystem an opportunity to bat around ideas, share experiences, and ask for feedback from fellow experts. We intend the workshop to have an informal and interactive feel, with a flexible timetable and plenty of room for ad-hoc discussion, demos, and impromptu short talks. Scope and target audience ------------------------- It is important to distinguish the Haskell Implementors' Workshop from the Haskell Symposium which is also co-located with ICFP 2009. The Haskell Symposium is for the publication of Haskell-related research. In contrast, the Haskell Implementors' Workshop will have no proceedings -- although we will aim to make slides and talk videos available with the consent of the speakers. In the Haskell Implementors' Workshop we hope to study the underlying technology. We want to bring together anyone interested in the nitty gritty details necessary to turn a text file into a deployed product. Having said that, members of the wider Haskell community are more than welcome to attend the workshop -- we need your feedback to keep the Haskell ecosystem thriving. The scope covers any of the following topics. There may be some topics that people feel we've missed, so by all means submit a proposal even if it doesn't fit exactly into one of these buckets: * Compilation techniques * Language features and extensions * Type system implementation * Concurrency and parallelism: language design and implementation * Performance, optimisation and benchmarking * Virtual machines and run-time systems * Libraries and Tools for development or deployment Talks ----- At this stage we would like to invite proposals from potential speakers for a relatively short talk. We are aiming for 20 min talks with 10 minutes for questions and changeovers. Please submit a talk title and abstract of no more than 200 words to simonmar(a)microsoft.com We want to hear from people writing compilers, tools, or libraries, people with cool ideas for directions in which we should take the platform, proposals for new features to be implemented, and half-baked crazy ideas. We will also have a lightning talks session which will be organised on the day. Organizers ---------- * Jean-Philippe Bernardy (Chalmers University of Technology) * Duncan Coutts - co-chair (Well-Typed LLP) * Iavor Diatchki (Galois) * Simon Marlow - co-chair (Microsoft Research) * Ben Lippmeier (University of New South Wales) * Neil Mitchell (Standard Chartered)

1 0

CFP: VSTTE workshops on Theory and on Experiments & Tools
by Gudmund Grov 15 Apr '10

15 Apr '10

------ Apologies for multiple copies ------ VSTTE 2010: Workshops on Theories, Tools and Experiments Edinburgh, Scotland, 19th August 2010 The Third International Conference on Verified Software: Theories, Tools, and Experiments (VSTTE) is part of the Verified Software Initiative (VSI), a fifteen-year, cooperative, international project directed at the scientific challenges of large-scale software verification. VSTTE will host two workshops: * VS-Theory focuses on theoretical foundations of software verification. Topics range from the difficult and essential study of soundness of delicate proof methods, to the discovery of new specification techniques and proof methods, to dramatic simplification or unification of existing methods, to as yet unknown breakthroughs. * VS-Tools & Experiments focuses on the development of verification tools and their experimental evaluation. Topics include interfaces between tools, tool integration platforms, and case studies. The workshops will provide a forum to present new, possibly unfinished work and will also give the opportunity to propose research challenges, which will help form a research agenda for the Verified Software Initiative. For further details, see the workshop web site: http://www.macs.hw.ac.uk/vstte10/Workshops.html Submissions Papers must be written in English using Springer LNCS style. The page limit is 10 pages for technical papers and 5 pages for proposals of verification challenges. The proceedings will be published as a technical report. Details on the submission process are available at http://www.macs.hw.ac.uk/vstte10/Workshops.html. Important Dates Submission: May 21, 2010 Notification: June 25, 2010 Final version: July 23, 2010 Workshops: August 19, 2010, 9am-1pm Chairs * VS-Theory is co-chaired by David Naumann, Stevens Institute of Technology, USA and Hongseok Yang, Queen Mary, University of London, UK * VS-Tools & Experiments is co-chaired by Tiziana Margaria, University of Potsdam, Germany and Rajeev Joshi, NASA/JPL Laboratory for Reliable Software, USA -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.

1 0

PhD and postdoc position in China/UK
by Thomas ANBERREE 14 Apr '10

14 Apr '10

Hello, The University of Nottingham offers inter-campus （China/UK） funded PhD positions in functional programming and type theory and we are also seeking Marie Curie fellows in the same area. For details see: http://www.cs.nott.ac.uk/~tfa/ or keep reading. -- -- -- -- -- -- -- -- -- -- -- -- -- Inter-Campus PhD studies in China/U.K. -- -- -- -- -- -- -- -- -- -- -- -- -- The Division of Computer Science at the University of Nottingham Ningbo China has several openings for PhD studies. The PhD scholarships are funded (some fully funded and some partially funded) by the University of Nottingham for a period of three years. Students are expected to spend one year in China, one year in the UK and the final year in China, under the supervision of two co-supervisors, one on each Campus. The expected starting date is October 2010. We are seeking to recruit candidates to work with us at the Functional Programming Laboratory, on a subject in relation to a new project: Implementation of a dependently-typed programming language using a verified core-language. The supervisors will be: Dr Thomas Anberree in China, Dr Thorsten Altenkirch in Nottingham. Applicants should have a degree in Computer Science or a related discipline and a strong background in functional programming and foundations of mathematics. Previous interest in dependent type theory is desirable. Excellent communication skills and English are required. Interested candidates should make initial inquiries by email to Thomas.Anberree(a)nottingham.edu.cn and include a CV. -- -- -- -- -- -- -- -- Marie Curie Fellowships -- -- -- -- -- -- -- -- The department of Computer Science at the University of Nottingham Ningbo China (UNNC) is keen to host Marie Curie Fellows . Candidates must have a PhD and preferably a few years of Post-Doctoral experience in the area of Functional Programming and Dependent Types Theory or other highly related area. Ideally, candidates will be citizens of a continental Europe country (i.e. a non-British European citizen), although British citizens may be considered. We are particularly seeking candidates to work on a new project, Implementation of a dependently-typed programming language based on a verified core language. The fellow will be a member of our Functional Programming Laboratory and will work under the supervision of Dr Thomas Anberree in China, Dr Thorsten Altenkirch in Nottingham. In the first instance interested candidates should direct informal enquiries to Thomas.Anberree(a)nottingham.edu.cn as soon as possible in order to put forward a Marie Curie Fellowship application. The University of Nottingham has an excellent track record with a high rate of successful applications and provides strong support in the application process. The closing deadline for applications is 30th June, and notifications will be made around the end of November. The appointment will be expected to begin around January 2011. UNNC can offer many of the support facilities which are on offer at the University of Nottingham in the United Kingdom. This is an ideal opportunity for the candidate to spend 12 to 24 months living and working in China, before returning to their home University. Thomas Anberree Division of Computer Science Office AB324 University of Nottingham Ningbo in China 199 Taikang East Road University Park Ningbo 315100 China Tel. +86 (0)574 8818 0217 Fax. +86 (0)574 8818 0125 邮编：315100 地址：宁波市高教园区泰康东路199号 ******************************************************************************************************************************* This email has been scanned by the Altman Email Security System. For more information please visit www.altman.co.uk/emailsystems *******************************************************************************************************************************

1 0

WWV'10: Deadline extension
by Temur Kutsia 13 Apr '10

13 Apr '10

[Apologies if you receive multiple copies] *********************************************************** * CALL FOR PAPERS * * * * WWV 2010 * * Automated Specification and Verification of Web Systems * * 6th International Workshop * * * * Vienna University of Technology, Austria * * July 30-31, 2010 * * http://www.complang.tuwien.ac.at/WWV2010/ * *********************************************************** *************** EXTENDED DEADLINES *************** Abstract Submission April 26, 2010 Full Paper Submission May 3, 2010

1 0

ANNOUNCE: darcs 2.4.1
by Reinier Lamers 12 Apr '10

12 Apr '10

Hi all, The darcs team would like to announce the immediate availability of darcs 2.4.1. This release fixes a number of issues that were found in darcs 2.4. The most important of these issues were that darcs did not work on Windows shares, and that darcs would not work if it was built with a wrong version of the mmap package. The easiest way to install darcs is using the Haskell Platform [1]. If you have installed the Haskell Platform or cabal-install, you can install this release by doing: $ cabal update $ cabal install --reinstall darcs Alternatively, you can download the tarball from http://darcs.net/releases/darcs-2.4.1.tar.gz and build it by hand as explained in the README file. What's New ---------- * Important changes in Darcs 2.4.1 * darcs works again on Windows network shares * missing documentation and test files have been added to the tarball * darcs will no longer give errors about a nonexistent file when compiled with the wrong mmap * moving files between directories can no longer break the directory index * darcs handles the case that someone uses 'remove -r' on an untracked directory * darcs ignores symlinks again, like all pre-2.4 releases * Bugs Fixed in Darcs 2.4.1 * 1645: ignore symlinks * 1750: uncover help text for 'darcs show pristine' * 1753: restrict mmap to version used by hashed-storage * 1754: fix issue458.sh on systems with xattrs * 1756: moving files between directories breaks index * 1757: add test files to distribution tarball * 1765: refuse to remove non-tracked directories recursively * 1767: send CRC erros to standard error Reporting bugs -------------- If you have an issue with darcs 2.4.1, you can report it via the web on http://bugs.darcs.net/ . You can also report bugs by email to bugs(a)darcs.net. Kind Regards, the darcs release manager, Reinier Lamers [1]: You can download the Haskell platform from http://hackage.haskell.org/platform/

1 0

All LazyFoo's SDL tutorials ported to Haskell
by Korcan Hussein 12 Apr '10

12 Apr '10

http://github.com/snkkid/LazyFooHaskell I hope somebody finds it useful. At some point I would like to cabalize this and put it up on hackage and maybe later I will branch a literate version but right now I feel like starting new related projects in Haskell :) _________________________________________________________________ http://clk.atdmt.com/UKM/go/197222280/direct/01/ Do you have a story that started on Hotmail? Tell us now

1 0