- Haskell - Haskell.org

LOPSTR/PPDP 2010 Final Call for Participation
by Temur Kutsia 05 Jul '10

05 Jul '10

[Apologize for multiple copies] ==================================================================== *** CALL FOR PARTICIPATION *** LOPSTR 2010 20th International Symposium on Logic-Based Program Synthesis and Transformation http://www.risc.jku.at/conferences/lopstr2010/ July 23-25, 2010 PPDP 2010 12th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming http://www.risc.jku.at/conferences/ppdp2010/ July 26-28, 2010 Hagenberg, Austria ==================================================================== IMPORTANT INFORMATION Early registration deadline (for both conferences): July 12, 2010 -------------------------------------------------------------------- LOPSTR 2010 INVITED SPEAKERS: - Bruno Buchberger (RISC, Johannes Kepler University Linz, Austria) - Olivier Danvy (University of Aarhus, Denmark) - Johann Schumann (RIACS/NASA Ames Research Center, USA) LOPSTR 2010 PROGRAM: http://www.risc.jku.at/conferences/lopstr2010/program.html -------------------------------------------------------------------- PPDP 2010 INVITED SPEAKERS: - Maria Paola Bonacina (University of Verona, Italy) - Sumit Gulwani (Microsoft Research) PPDP 2010 PROGRAM: http://www.risc.jku.at/conferences/ppdp2010/program.html --------------------------------------------------------------------

1 0

TLDI 2011 Call For Papers
by Stephanie Weirich 02 Jul '10

02 Jul '10

TLDI 2011 CALL FOR PAPERS The Sixth ACM SIGPLAN Workshop on Types in Language Design and Implementation Austin, Texas, USA Tuesday, January 25, 2011 (Co-located with POPL 2011) http://www.mpi-sws.org/~dreyer/tldi2011/ Submission Deadline: October 11, 2010 The role of types and proofs in all aspects of language design, compiler construction, and software development has expanded greatly in recent years. Type systems, type-based analyses and type-theoretic deductive systems have been central to advances in compilation techniques for modern programming languages, verification of safety and security properties of programs, program transformation and optimization, and many other areas. The ACM SIGPLAN Workshop on Types in Language Design and Implementation brings researchers together to share new ideas and results concerning all aspects of types and programming, and is now an annual event. TLDI 2011 is the sixth workshop in the series and will be co-located with POPL in Austin, Texas in January 2011. Submissions for TLDI 2011 are invited on all interactions of types with language design, implementation, and programming methodology. This includes both practical applications and theoretical aspects. TLDI 2011 specifically encourages papers from a broad field of programming language and compiler researchers, including those working on object-oriented or dynamic languages, systems programming, mobile-code or security, as well as traditional fully-static type systems. Topics of interest include: * Typed intermediate languages and type-directed compilation * Type-based language support for safety and security * Types for interoperability * Type systems for system programming languages * Type-based program analysis, transformation, and optimization * Dependent types and type-based proof assistants * Types for security protocols, concurrency, and distributed computing * Type inference and type reconstruction * Type-based specifications of data structures and program invariants * Type-based memory management * Proof-carrying code and certifying compilation * Types and objects This is not meant to be an exhaustive list; papers on novel utilizations of type information are welcome. Authors concerned about the suitability of a topic are encouraged to inquire via electronic mail to the program chair prior to submission. Submission Guidelines: Authors should submit a full paper of no more than 12 pages (including bibliography and appendices) by Monday, October 11, 2010. The submission deadline and length limitations are firm. Submissions that do not meet these guidelines will not be considered. All submissions should be in standard ACM SIGPLAN conference format: two columns, nine-point font on a ten-point baseline. Detailed formatting guidelines are available on the SIGPLAN Author Information page, along with a LaTeX class file and template. Papers must be submitted electronically via the workshop website (http://www.mpi-sws.org/~dreyer/tldi2011/) in Adobe Portable Document Format (PDF) and must be formatted for US Letter size (8.5"x11") paper. Authors for whom this is a hardship should contact the program chair before the deadline. Submitted papers must adhere to the SIGPLAN Republication Policy. Submissions should contain original research not published or submitted for publication elsewhere. Publication: As in previous years, accepted papers will be published by the ACM and appear in the ACM digital library. A printed proceedings will be available at the workshop. Important Dates: - Submission deadline: October 11, 2010 (Monday), 21:00 Samoa-Apia Time - Notification: November 8, 2010 (Monday) - Final versions due: November 22, 2010 (Monday) - Workshop: January 25, 2011 (Tuesday) General Chair: Stephanie Weirich University of Pennsylvania sweirich at cis dot upenn dot edu Program Chair: Derek Dreyer Max Planck Institute for Software Systems (MPI-SWS) dreyer at mpi-sws dot org Program Committee: Thorsten Altenkirch (University of Nottingham) Fritz Henglein (University of Copenhagen) Michael Hicks (University of Maryland, College Park) Limin Jia (Carnegie Mellon University) Mark Jones (Portland State University) Neel Krishnaswami (Microsoft Research, Cambridge) Paul-André Melliès (CNRS & Université Paris Diderot) Aleks Nanevski (IMDEA Software, Madrid) Benjamin Pierce (University of Pennsylvania) Tachio Terauchi (Tohoku University) Sam Tobin-Hochstadt (Northeastern University) Steering Committee: Amal Ahmed (Indiana University) Nick Benton (Microsoft Research, Cambridge) Derek Dreyer (MPI-SWS) Robert Harper (Carnegie Mellon University, chair) Andrew Kennedy (Microsoft Research, Cambridge) Francois Pottier (INRIA Rocquencourt) Zhong Shao (Yale University) Stephanie Weirich (University of Pennsylvania)

1 0

Delivery reports about your e-mail
by jon.fairbairn＠cl.cam.ac.uk 02 Jul '10

02 Jul '10

The message was undeliverable due to the following reason(s): Your message could not be delivered because the destination server was unreachable within the allowed queue period. The amount of time a message is queued before it is returned depends on local configura- tion parameters. Most likely there is a network problem that prevented delivery, but it is also possible that the computer is turned off, or does not have a mail system running right now. Your message could not be delivered within 1 days: Server 206.198.95.174 is not responding. The following recipients did not receive this message: <haskell(a)haskell.org> Please reply to postmaster(a)cl.cam.ac.uk if you feel this message to be in error.

1 0

ANNOUNCE: HaRe, the Haskell Refactorer 0.6
by Chris BROWN 28 Jun '10

28 Jun '10

Dear Haskellers, As part of our project on Refactoring Functional Programs http://www.cs.kent.ac.uk/projects/refactor-fp/ we are pleased to announce the availability of HaRe 0.6 (also known as HaRe 28/06/2010), a snapshot of our Haskell Refactorer prototype. Apart from bug-fixes, there are major changes since HaRe 0.5 and HaRe 0.4: A number of new refactorings have been added to HaRe. Some of these include: Adding and removing fields and constructors to data-type definitions, folding and unfolding against as-patterns, merging and splitting, converting between let and where constructs, introduce pattern matching, generative folding, and a clone detection and elimination tool. We have evolved the ongoing architecture of HaRe and derived an API (documented using Haddock) for program analysis and transformation. This allows HaRe to serve as a framework for end-users to build their own refactorings or just program transformations (or analyses). HaRe is available to download directly from here: http://www.cs.kent.ac.uk/projects/refactor-fp/hare/HaRe_28062010.tar.gz You can get HaRe 0.6 and the documentation about how to build your own refactorings via: http://www.cs.kent.ac.uk/projects/refactor-fp/hare.html Please see the README.txt for build/use instructions and known issues, and let us know about any problems, bugs, suggestions or additional platforms you can confirm as working. You will need: 1. ghc-6.12.1 2. hint-0.3.2.3 (available from cabal) 3. unix/gnu tools (or cygwin tools, if on windows) 4. vim or emacs (we've tested with gvim 6.2 and with emacs 21.4) 5. If you intend on running the test suite, HUnit-1.0. Happy Refactoring! The HaRe Team (Chris Brown, Huiqing Li, Simon Thompson) Project email: refactor-fp at kent.ac.uk<http://www.haskell.org/mailman/listinfo/haskell> Background: Refactoring is the process of changing the structure of programs without changing their functionality, i.e., refactorings are meaning-preserving program transformations that implement design changes. For more details about refactoring, about our project and for background on HaRe, see our project pages. HaRe - the Haskell Refactorer: HaRe is our prototype tool supporting a collection of refactorings for Haskell 98 (see README.txt for known issues and limitations). It is implemented as a separate refactoring engine (on top of Programatica's Haskell frontend and Strafunski's generic traversal strategy library), with small scripting frontends that call this engine from either Vim or Emacs. Currently supported refactorings: Introduce Pattern Match : place cursor over pattern variable Introduce Sub pattern : place cursor over pattern variable Introduce Case Expression : place cursor over pattern variable Generative Fold : highlight expression to fold. Must have equation in comment directly before definition of highlighted expression. Clone Analysis : select from menu Clone Extraction : highlight clone from the clone class to extract, follow step-by-step instructions. Converting Let to Where : place cursor at start of identifier whose definition is to be moved Converting Where to Let : place cursor at start of identifier whose definition is to be moved. create type signatures : select from menu remove redundant declarations : highlight definition to clean up add constructor to data type : place cursor at start of data type, you'll be prompted to add the new Constructor name, followed by any Type parameters as a complete string Split a tuple : place cursor at start of top level definition that returns a tuple. Slicing based on a subexpression : highlight sub-expression to extract. Instantiate a general pattern : select a function equation and enter the new instances for each pattern in the argument set. Extract an expression : highlight an expression within a definition Convert data type to newtype : place cursor at start of data type add definition to merge : place cursor at start of definition that is to be merged merge definitions : use "add definition for merge" for each definition to be merged. then choose merge definitions from menu. fold function definition : highlight function equation to fold against. fold constant definition : highlight constant equation to fold against. convert pattern to an as pattern : highlight pattern to convert. unfold references to as patterns : place cursor over as pattern name. remove field from a data type : place cursor at start of field to remove. add field to data type : place cursor over start of constructor. enter new field name. add debug information : add trace calls to function by placing cursor at the start of the function to trace rename : place cursor at start of identifier to be renamed, you'll be prompted for a new name Lift def to top level : place cursor at start of identifier whose definition is to be moved Lift def one level : place cursor at start of identifier whose definition is to be moved Demote : place cursor at start of identifier whose definition is to be moved Introduce new def : highlight expression to be named, you'll be prompted for a new name Unfold def : place cursor at start of identifier where its definition is to be unfolded Generalise def : place cursor at start of identifier where its definition is to be unfolded Remove def : place cursor at start of identifier whose definition is to be removed Duplicate def : place cursor at start of identifier whose definition is to be duplicated, you'll be prompted for a new name Add one parameter : place cursor at start of identifier whose definition is to be modified, you'll be prompted for a new name rm one parameter : place cursor in formal parameter which is to be removed Move def to another module : place cursor at start of the identifier whose definition is to be moved, you'll be prompted for the module name Clean imports : cursor position does not matter, just choose the command from the refactor menu Make import explicit : place cursor at the start of the module name in the import declaration Add to export : place cursor at start of the identifier which is to be added to the export Remove from export : place cursor at start of the entry to be removed in the export list From concrete to abstract data type: place cursor at start of the data type name Add field names : place cursor at start of the data type name Add discriminators : place cursor at start of the data type name Add constructors : place cursor at start of the data type name Eliminate nested patterns : place cursor at start of the data type name Eliminate patterns : place cursor at start of the data type name Create an ADT module : place cursor at start of the data type name Eliminate intermediate list: cursor position does not matter, just choose the command from the menu. Caveats (see also README.txt): Please keep in mind that this is a prototype, so we do not recommend to use it on your productions sources just yet. Just play with it to get an idea of tool-supported refactoring in Haskell, and send us your feedback and bug-reports. Our goal is to develop this into a tool that many of you will find indispensable for Haskell development. Regards, The HaRe team.

1 0

CfP ADAPT Summer School
by Ralf Laemmel 23 Jun '10

23 Jun '10

Dear Haskellers, this summer school contains bits of formal methods and language design that typically intersect very well with interests on this list. Looking forward to meet some of you in Koblenz. Ralf 8< - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - CALL FOR PARTICIPATION : ADAPT 2010 1st ADAPT Summer School September 26 - October 2, 2010, Koblenz, Germany http://adapt.uni-koblenz.de/summerschool2010 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - Software adaptation is a topic that crosscuts much of software engineering, programming languages, information systems, formal methods, and other major areas of computer science. The CS department at the University of Koblenz-Landau engages in a research focus on software adaptation, and thereby connects scientists and teams in classical areas of computer science as much as application areas such as web-based systems, SOA, mobile systems, and robotics. ADAPT 2010 is the first edition in a series of summer schools on software adaptation. The program of ADAPT 2010 appeals to PhD students and possibly specialized Master's students in computer science. 8< - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -

1 0

Call for Participation: SICSA Summer School on Formal Reasoning & Representation of Complex Systems
by Gudmund Grov 23 Jun '10

23 Jun '10

*** Apologies for multiple copies *** Call for Participation ----------------------- SSFRR 2010 SICSA Summer School on Formal Reasoning & Representation of Complex Systems 14-15 August 2010 -- Heriot-Watt University campus -- Edinburgh Satellite summer school of VSTTE 2010 http://dream.inf.ed.ac.uk/events/ssfrr-2010/ ---------------------- ABOUT --------- 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; process algebras and formal analysis of security. 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. PRESENTERS --------- 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) * Jane Hillston (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) REGISTRATION --------- Registration is available from: http://www.macs.hw.ac.uk/vstte10_reg/Registration.php The registration fee is £110, which also covers materials and lunches. Accommodation at the Heriot-Watt campus (£42.50 per night incl. VAT and breakfast) can be including with your booking when you register. This is highly recommended since the summer school will coincide with several of the famous Edinburgh festivals -- where hotel prices in town tend to be very inflated. SICSA will cover registration and two nights campus accommodation for SICSA students (students from most Scottish Universities -- see http://www.sicsa.ac.uk/ to check if you are eligible). The number of SICSA students is limited, and a decision on ranking if this number is exceeded will only be taken if necessary. PRELIMINARY PROGRAM --------- The summer school has the following preliminary program (timing and titles may still change): Saturday: * 09:00: Registration * 09:30: J Moore -- Machines Reasoning about Machines - 39 Years and Counting * 11:00: Coffee break * 11:30: Gerwin Klein -- Specification and Refinement in Operating System Verification * 13:00: Lunch * 14:00: Bob Atkey/Ewen Maclean -- Amortised Resource Analysis and Functional Correctness with Separation Logic * 15:30: Coffee break * 16:00: Alan Bundy/Lucas Dixon -- Proof-planning, inductive reasoning, and beyond * 17:30: End Sunday: * 09:30: Natarajan Shankar -- Verification using SAT and SMT solvers * 11:00: Coffee break * 11:30: Graham Steel -- Formal Analysis of Key Management APIs * 13:00: Lunch * 14:00: Cliff Jones -- Tackling concurrency by reasoning explicitly about inference * 15:30: Coffee break * 16:00: Jane Hillston -- From Milner to Markov and Back: Stochastic process algebras and their equivalence relations * 17:30: End VENUE --------- The summer school is a satellite event of VSSTE 2010 (see http://www.macs.hw.ac.uk/vstte10/) and will be held the two days before the main event: Saturday 14th and Sunday 15th August 2010. Like VSTTE 2010, it will be held at the Edinburgh campus of Heriot-Watt University. ORGANISERS --------- The summer school is jointly organised by The School of Informatics at Edinburgh University and The School of Mathematical and Computer Sciences at Heriot-Watt University by: * Lucas Dixon (Edinburgh) * Gudmund Grov (Edinburgh) * Ewen Maclean (Heriot-Watt) CONTACT --------- The organisers can be contacted at the following email address: ssfrr-2010(a)inf.ed.ac.uk. -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.

1 0

Announce: revamped free theorems generator
by Janis Voigtländer 23 Jun '10

23 Jun '10

The online free theorems generator, previously announced here: http://www.haskell.org/pipermail/haskell/2007-October/019917.html now runs at: http://www-ps.iai.uni-bonn.de/ft Thanks to Matthias Bartsch, there are now additional features in the online tool. In particular, one can declare one's own algebraic data types, type synonyms, type renamings, and type classes, and then generate free theorems for types involving those. Also, the tool now outputs inline graphics with nicely typeset theorems. (Plain text output, as well as .pdf and corresponding .tex, are still possible.) Ciao, Janis. -- Jun.-Prof. Dr. Janis Voigtländer http://www.iai.uni-bonn.de/~jv/ mailto:jv@iai.uni-bonn.de

4 13

Re: [Haskell] Announce: revamped free theorems generator
by Janis Voigtländer 18 Jun '10

18 Jun '10

rossberg(a)mpi-sws.org schrieb: >> The online free theorems generator, previously announced here: >> >> http://www.haskell.org/pipermail/haskell/2007-October/019917.html >> >> now runs at: >> >> http://www-ps.iai.uni-bonn.de/ft > > I don't quite understand. Isn't that tool basically just giving you the > (unfolded) definition of logical relatedness at the type you enter? Although > pretty "free", that is not yet a "free theorem", at least not as I am used > to see this term used. For example, a free theorem for type a -> a would be > the property forall f :: a -> a, forall e, f e = e. I wouldn't say that statements of this form, completely determining the function definition from the function's type, are what it needs to qualify as a free theorem. For one thing, that's only possible for very simple types. For example, what would you say is a "not just unfolding the definition of the logical relation"-style free theorem for the type [a] -> [a]? For the type a -> a you mention, the generator gives the property forall f :: a -> a, forall g, forall x, g (f x) = f (g x). I wouldn't say that this is just unfolding the definition of logical relatedness. But maybe more interestingly, consider type (a -> Bool) -> [a] -> [a]. The generator answers: forall f :: (a -> Bool) -> [a] -> [a], forall g, forall p, forall q, (forall x, p x = q (g x)) => (forall y, map g (f p y) = f q (map g y)) I'd say that this *is* typically referred to as the free theorem corresponding to filter's type, namely that the property map g . filter (q . g) = filter q . map g holds for all like-wise typed functions. In any case, I would be very interested in learning more about for what and where you are used to see the term "free theorems" used, as I am always interested in new applications of parametricity. I can just say that myself I am very used to calling statements like the one about filter above "free theorems". Ciao, Janis. -- Jun.-Prof. Dr. Janis Voigtländer http://www.iai.uni-bonn.de/~jv/ mailto:jv@iai.uni-bonn.de

1 0

Fully-funded PhD in programming languages at Oxford
by Jeremy.Gibbons＠comlab.ox.ac.uk 17 Jun '10

17 Jun '10

FULLY-FUNDED DOCTORAL STUDENTSHIP IN PROGRAMMING LANGUAGES AT OXFORD I have just obtained funding for a DPhil studentship at Oxford. The studentship is open in terms of topic; I would welcome applications for research in any of my areas of interest. These include: functional programming generic programming dependent types design patterns model-driven development For more information about topics, please visit my web page http://web.comlab.ox.ac.uk/people/Jeremy.Gibbons/ or discuss with me. The successful candidate will have a good bachelor's or master's degree in CS, and a strong background in the principles of programming languages. The funding covers stipend, fees (at the home/EU rate), equipment, and travel, and is for three and a half years from October 2010 (or as soon as possible after that). Please do contact me with any questions, and in any case before applying. Please also pass this note on to anyone who might be interested. Jeremy.Gibbons(a)comlab.ox.ac.uk, Deputy Director Oxford University Computing Laboratory, TEL: +44 1865 283508 Wolfson Building, Parks Road, FAX: +44 1865 283531 Oxford OX1 3QD, UK. URL: http://www.comlab.ox.ac.uk/oucl/people/jeremy.gibbons.html

1 0

LOPSTR/PPDP 2010 Early Registration Deadline: June 21
by Temur Kutsia 15 Jun '10

15 Jun '10

[Apologize for multiple copies] ==================================================================== *** CALL FOR PARTICIPATION *** LOPSTR 2010 20th International Symposium on Logic-Based Program Synthesis and Transformation http://www.risc.jku.at/conferences/lopstr2010/ July 23-25, 2010 PPDP 2010 12th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming http://www.risc.jku.at/conferences/ppdp2010/ July 26-28, 2010 Hagenberg, Austria ==================================================================== IMPORTANT INFORMATION Early registration deadline (for both conferences): June 21, 2010 -------------------------------------------------------------------- LOPSTR 2010 INVITED SPEAKERS: - Bruno Buchberger (RISC, Johannes Kepler University Linz, Austria) - Olivier Danvy (University of Aarhus, Denmark) - Johann Schumann (RIACS/NASA Ames Research Center, USA) LOPSTR 2010 PROGRAM: http://www.risc.jku.at/conferences/lopstr2010/program.html -------------------------------------------------------------------- PPDP 2010 INVITED SPEAKERS: - Maria Paola Bonacina (University of Verona, Italy) - Sumit Gulwani (Microsoft Research) PPDP 2010 PROGRAM: http://www.risc.jku.at/conferences/ppdp2010/program.html --------------------------------------------------------------------

1 0