- Haskell - Haskell.org

Re: [Haskell] [Haskell-cafe] ANN: reform - a type-safe form generation and validation library in the spirit of formlets and digestive-functors < 0.2
by Jeremy Shaw 22 May '12

22 May '12

Sounds great! I have some vague ideas about what the comparison might reveal -- but I expect to learn quite a bit in the process, and use that to improve reform. There is definitely room for more than one form validation library. They all have shortcomings, and I am hoping something even better will come along some day :) - jeremy On Tue, May 22, 2012 at 4:31 AM, Jasper Van der Jeugt <m(a)jaspervdj.be> wrote: > Congrats on the release! > > I would like to help out with the full comparison since I have some > knowledge and experience on the subject. Because of the different > approach, I think there's definitely room for two libraries. > > Cheers, > Jasper > > On Tue, May 22, 2012 at 2:23 AM, Felipe Almeida Lessa > <felipe.lessa(a)gmail.com> wrote: >> On Mon, May 21, 2012 at 7:18 PM, Jeremy Shaw <jeremy(a)n-heptane.com> wrote: >>> I hope to do a full comparison of reform vs digestive-functors 0.3 vs >>> yesod forms in a few weeks. >> >> That would be awesome! Just sayin' =). >> >> Cheers, >> >> -- >> Felipe. >> >> -- >> You received this message because you are subscribed to the Google Groups "HAppS" group. >> To post to this group, send email to happs(a)googlegroups.com. >> To unsubscribe from this group, send email to happs%2Bunsubscribe(a)googlegroups.com. >> For more options, visit this group at http://groups.google.com/group/happs?hl=en. >> > > _______________________________________________ > Haskell-Cafe mailing list > Haskell-Cafe(a)haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe

1 0

ANN: reform - a type-safe form generation and validation library in the spirit of formlets and digestive-functors < 0.2
by Jeremy Shaw 22 May '12

22 May '12

I am pleased to annouce the release of 'reform'. A full tutorial is available here: http://www.happstack.com/docs/crashcourse/Reform.html Reform is an HTML form generation and validation library. It follows in the footsteps of formlets and digestive-functors <= 0.2. In fact, much of the code in reform comes from the digestive-functors-0.2 code base. Reform is designed to be usuable with a wide variety of Haskell web servers and templating libraries. You can find the following packages on hackage: * reform - the core library * reform-happstack - support for using reform with the Happstack server * reform-blaze - support for creating forms for blaze-html * reform-hsp - support for creating forms for HSP (another xml/html template library) The source code is available via darcs: darcs get http://patch-tag.com/r/stepcut/reform The darcs repo also includes proof-of-concept support for 'Heist'. Reform will feel very familiar to formlets and digestive-functors <= 0.2 users. The primary motivation behind this library is to provide a supported alternative to digestive-functors 0.2 for users that prefer 0.2 over 0.3. The key new feature in reform is the ability to separate the validation code from the view generation code. This allows library authors to provide validators (known as Proofs) which the users can use when constructing their forms. The proof names appear in the type-signatures. This allows the library author to ensure that the value returned by a user created form is not merely the correct type, but has also passed validation. The reform-happstack package also provides simple and transparent Cross-Site Request Forgery (CSRF) protection, using the double-submit method. This method has some weaknesses. For example, I believe it can be circumvented if your site is vulnerable to cross-site scripting (XSS) attacks. If you have suggestions on how to improve the CSRF protection -- please let us know! I hope to do a full comparison of reform vs digestive-functors 0.3 vs yesod forms in a few weeks. - jeremy

2 1

CUFP 2012: Call for Presentations
by Stefan Wehr 21 May '12

21 May '12

Hi everyone, just a quick reminder: the talk submission proposal for this year's CUPF is 29 June 2012. If you have something interesting to say about commercial applications of functional programming languages (especially Haskell, of course!), please submit a proposal. Thanks, Stefan COMMERCIAL USERS OF FUNCTIONAL PROGRAMMING 2012 CUFP 2012 http://cufp.org/conference CALL FOR PRESENTATIONS Copenhagen, Denmark Sep 13-15 Co-located with ICFP 2012 Sponsored by SIGPLAN Talk Proposal Submission Deadline 29 June 2012 The annual CUFP workshop is a place where people can see how others are using functional programming to solve real world problems; where practitioners meet and collaborate; where language designers and users can share ideas about the future of their favorite language; and where one can learn practical techniques and approaches for putting functional programming to work. Giving a CUFP Talk ================== If you have experience using functional languages in a practical setting, we invite you to submit a proposal to give a talk at the workshop. We're looking for two kinds of talks: Experience reports are typically 25 minutes long, and aim to inform participants about how functional programming plays out in real-world applications, focusing especially on lessons learned and insights gained. Experience reports don't need to be highly technical; reflections on the commercial, management, or software engineering aspects are, if anything, more important. Technical talks are also 25 minutes long, and should focus on teaching the audience something about a particular technique or methodology, from the point of view of someone who has seen it play out in practice. These talks could cover anything from techniques for building functional concurrent applications, to managing dynamic reconfigurations, to design recipes for using types effectively in large-scale applications. While these talks will often be based on a particular language, they should be accessible to a broad range of programmers. If you are interested in offering a talk, or nominating someone to do so, send an e-mail to sperber(at)deinprogramm(dot)de or avsm2(at)cl(dot)cam(dot)ac(dot)uk by 29 June 2012 with a short description of what you'd like to talk about or what you think your nominee should give a talk about. Such descriptions should be about one page long. There will be a short scribes report of the presentations and discussions but not of the details of individual talks, as the meeting is intended to be more a discussion forum than a technical interchange. You do not need to submit a paper, just a proposal for your talk! Program Committee ================= Mike Sperber (Active Group), co-chair Anil Madhavapeddy (University of Cambridge), co-chair Ashish Agarwal (New York University) Thomas Arts (QuviQ AB) Chris Houser (LonoCloud) Tomas Petricek (University of Cambridge) Heiko Seeberger (Typesafe) Stefan Wehr (factis research) Noel Welsh (untyped) More information ================ For more information on CUFP, including videos of presentations from previous years, take a look at the CUFP website at http://cufp.org. Note that presenters, like other attendees, will need to register for the event. Presentations will be video taped and presenters will be expected to sign an ACM copyright release form. Acceptance and rejection letters will be sent out by July 16th. Guidance on giving a great CUFP talk ==================================== Focus on the interesting bits: Think about what will distinguish your talk, and what will engage the audience, and focus there. There are a number of places to look for those interesting bits. Setting: FP is pretty well established in some areas, including formal verification, financial processing and server-side web-services. An unusual setting can be a source of interest. If you're deploying FP-based mobile UIs or building servers on oil rigs, then the challenges of that scenario are worth focusing on. Did FP help or hinder in adapting to the setting? Technology: The CUFP audience is hungry to learn about how FP techniques work in practice. What design patterns have you applied, and to what areas? Did you use functional reactive programming for user interfaces, or DSLs for playing chess, or fault-tolerant actors for large scale geological data processing? Teach us something about the techniques you used, and why we should consider using them ourselves. Getting things done: How did you deal with large software development in the absence of a myriad of pre-existing support that are often expected in larger commercial environments (IDEs, coverage tools, debuggers, profilers) and without larger, proven bodies of libraries? Did you hit any brick walls that required support from the community? Don't just be a cheerleader: It's easy to write a rah-rah talk about how well FP worked for you, but CUFP is more interesting when the talks also spend time on what doesn't work. Even when the results were all great, you should spend more time on the challenges along the way than on the parts that went smoothly.

1 0

WLPE 2012 - Call for papers
by Wim Vanhoof 21 May '12

21 May '12

[Apologies for multiple copies...] ----------------------------------------------------------- WLPE 2012 - CALL FOR PAPERS Workshop on Logic-based Methods in Programming Environments (satellite workshop of ICLP 2012) September 8, 2012 Budapest, Hungary http://users.dsic.upv.es/workshops/wlpe2012/ ----------------------------------------------------------- The workshop aims at providing an informal meeting for researchers working on logic-based tools for development and analysis of programs. In addition to papers describing more conceptual work on environmental tools, we solicit papers describing the implementation of and experimentation with such tools. We hope to attain the same friendly atmosphere as in past workshops, which enabled fruitful exchanges leading to joint research and subsequent publications. Areas particularly relevant to the workshop include: * static and dynamic analysis * debugging and testing * program verification and validation * code generation from specifications * termination and non-termination analysis * reasoning on occurs-check freeness and determinacy * frameworks and resources for sharing in the logic programming community * profiling and performance analysis * type- and mode analysis * shape, point-to and escape analysis * module systems * optimization tools * program understanding * refactoring * logical meta-languages Note that this list is not exhaustive and, if you are interested in taking part in the workshop but unsure if your work falls within its scope, do contact the organisers who will be happy to advise. The 22nd Workshop on Logic-based methods in Programming Environments will take place in Budapest, Hungary, as a satellite workshop of ICLP 2012, the 28the International Conference on Logic Programming. This workshop will continue the series of successful international workshops on logic programming environments held in Ohio, USA (1989), Eilat, Israel (1990), Paris, France (1991), Washington, USA (1992), Vancouver, Canada (1993), Santa Margherita Ligure, Italy (1994), Portland, USA (1995), Leuven, Belgium and Port Jefferson, USA (1997), Las Cruces, USA (1999), Paphos, Cyprus (2001), Copenhagen, Denmark (2002), Mumbai, India (2003), Saint Malo, France (2004), Sitges, Spain (2005), Seattle, Washington USA (2006), Porto, Portugal (2007), Udine, Italy (2008), Pasadena, USA (2009), Edinburgh, UK (2010), and Odense, Denmark (2011). This year WLPE will be coordinated with CICLOPS. In particular, there will be two special events organised: (a) SWI-25, a celebration and retrospective of the open source SWI-Prolog engine on the occasion of its 25th birthday, and (b) OpenPL, an event on (1) coordinating efforts towards furthering cross-engine compatibility, with a focus on libraries and add-on packages, and (2) the creation of a user-contributing repository of Prolog code. Submission guidelines --------------------- We encourage the submission of original research in the area as well as relevant results that have been submitted, rejected, or accepted elsewhere as long as they are relevant for the WLPE community. All papers must be written in English and should not exceed 15 pages. We welcome also shorter submissions, e.g., extended abstracts and short papers, of at least 3 pages. Papers should be submitted electronically via the submission page: https://www.easychair.org/conferences/?conf=wlpe2012 An informal proceedings will be distributed electronically at the workshop. After the workshop, the proceedings will be publicly available on-line in the Computing Research Repository (CoRR). Important dates --------------- Submission: June 20, 2012 Notification: July 16, 2012 Camera-ready: July 27, 2012 Workshop: September 8, 2012 Workshop organizers ------------------- Win Vanhoof Faculty of Computer Science University of Namur Namur, Belgium Email: wlpe2012(a)dsic.upv.es Alicia Villanueva Department of Computer Science (DSIC) Universitat Politècnica de València Valencia, Spain Email: wlpe2012(a)dsic.upv.es Program committee ----------------- Salvador Abreu Universidade de Évora, Portugal Petra Hofstedt University of Technology Berlin, Germany Jacob Howe City University London, UK Yoshitaka Kameya Tokyo Institute of Technology, Japan Roland Kaminski Universität Postdam, Germany Lunjin Lu Oakland University, USA Alexander Serebrenik Eindhoven University of Technology, The Netherlands Peter Schneider-Kamp University of Southern Denmark, Denmark Zoltan Somogyi University of Melbourne, Australia Win Vanhoof University of Namur, Belgium Alicia Villanueva Universitat Politècnica de València, Spain Damiano Zanardini Universidad Politécnica de Madrid, Spain

1 0

CAV 2012: Call for Participation
by CAV 2012 CFP 17 May '12

17 May '12

====== CALL FOR PARTICIPATION ================================================== 24th International Conference on Computer Aided Verification (CAV 2012) July 7-13, 2012 Berkeley, California, USA Program Chairs: Madhusudan Parathasarathy and Sanjit A. Seshia Website: http://cav12.cs.illinois.edu/ Aims and Scope -------------------------------------------------------------------------------- The conference on Computer Aided Verification (CAV), 2012, is the 24th in a series dedicated to the advancement of the theory and practice of computer-aided formal analysis methods for hardware and software systems. CAV considers it vital to continue spurring advances in hardware and software verification while expanding to new domains such as biological systems and computer security. The conference covers the spectrum from theoretical results to concrete applications, with an emphasis on practical verification tools and the algorithms and techniques that are needed for their implementation. The proceedings of the conference will be published in the Springer-Verlag Lecture Notes in Computer Science series. A selection of papers will be invited to a special issue of Formal Methods in System Design and the Journal of the ACM. ** NEW in 2012 ** -------------------------------------------------------------------------------- CAV will have *special tracks* in the following four areas: 1. Hardware Verification (track chair: Andreas Kuehlmann) 2. Computer Security (track chair: Somesh Jha) 3. Embedded Systems (track chair: Stavros Tripakis) 4. SAT and SMT (track chair: Daniel Kroening) Invited Talks -------------------------------------------------------------------------------- - Wolfgang Thomas, RWTH Aachen University "Synthesis and Some of Its Challenges" - David Dill, Stanford University "Model Checking Cell Biology" - Alex Haldermann, University of Michigan On security of voting machines Invited Tutorials -------------------------------------------------------------------------------- - Rastislav Bodik and Emina Torlak, University of California, Berkeley "Synthesizing Programs with Constraint Solvers" - Aaron Bradley, University of Colorado at Boulder "IC3 and Beyond: Incremental, Inductive Verification" - Chris Myers, University of Utah "Formal Verification of Genetic Circuits" - Michał Moskal, Microsoft Research, Seattle "From C to infinity and back: Unbounded auto-active verification with VCC" ====== CONFERENCE PROGRAM ====================================================== Saturday July 7 - WORKSHOPS ---------------------------------------- - NSV 2012 5th International Workshop on Numerical Software Verification Co-chairs: Swarat Chaudhuri, Sriram Sankaranarayanan - (EC)^2 2012 Workshop on Exploiting Concurrency Efficiently and Correctly Co-chairs: Sebastian Burckhardt, Azadeh Farzan, Ganesh Gopalakrishnan, Stephen Siegel, Helmut Veith, Josef Widder - SYNT 2012 1st Workshop on Synthesis Co-chairs: Doron Peled, Sven Schewe - AMFSB 2012 Applications of Formal Methods in Systems Biology Co-chairs: Vincent Danos, Mahesh Viswanathan - LfSA 2012 Logics for System Analysis Co-chairs: André Platzer, Philipp Rümmer Sunday July 8 - WORKSHOPS ---------------------------------------- - NSV 2012 5th International Workshop on Numerical Software Verification Co-chairs: Swarat Chaudhuri, Sriram Sankaranarayanan - (EC)^2 2012 Workshop on Exploiting Concurrency Efficiently and Correctly Co-chairs: Sebastian Burckhardt, Azadeh Farzan, Ganesh Gopalakrishnan, Stephen Siegel, Helmut Veith, Josef Widder - SYNT 2012 1st Workshop on Synthesis Co-chairs: Doron Peled, Sven Schewe - AMFSB 2012 Applications of Formal Methods in Systems Biology Co-chairs: Vincent Danos, Mahesh Viswanathan - BOOGIE 2012 2nd International Workshop on Intermediate Verification Languages Chair: Zvonimir Rakamaric - REORDER 2012 First International Workshop on Memory Consistency Models Co-chairs: Sela Mador-Haim, Jade Alglave Monday July 9 - INVITED TUTORIALS ---------------------------------------- 8:30 - 10:00: "Synthesizing Programs with Constraint Solvers" (Ras Bodik and Emina Torlak) 10:00 - 10:30: Break 10:30 - 12:00: "IC3 and Beyond: Incremental, Inductive Verification" (Aaron Bradley) 12:00 - 1:30: Break 1:30 - 3:00: "Formal Verification of Genetic Circuits" (Chris Myers) 3:00 - 3:30: Break 3:30 - 5:00: "From C to infinity and back: Unbounded auto-active verification with VCC" (Michal Moskal) Tuesday July 10 ---------------------------------------- 8:30 - 9:00: Welcome 9:00 - 10:00: "Synthesis and Some of Its Challenges" (Wolfgang Thomas - Keynote) 10:00 - 10:30: Break 10:30 - 12:00: AUTOMATA AND SYNTHESIS R1 Jan Kretinsky and Javier Esparza "Deterministic Automata for the (F,G)-fragment of LTL" R2 Tomas Brazdil, Krishnendu Chatterjee, Antonin Kucera and Petr Novotny "Efficient Controller Synthesis for Consumption Games with Multiple Resource Types" R3 Rüdiger Ehlers "ACTL ∩ LTL Synthesis" T1 François Raskin "Acacia+, a tool for LTL synthesis" T2 Chih-Hong Cheng, Michael Geisinger, Harald Ruess, Christian Buckl and Alois Knoll "MGSyn: Automatic Synthesis for Industrial Automation" 12:00 - 1:30: Break 1:30 - 3:35: INDUCTIVE INFERENCE AND TERMINATION R4 Yu-Fang Chen and Bow-Yaw Wang "Learning Boolean Functions Incrementally" R5 Rahul Sharma, Aditya Nori and Alex Aiken "Interpolants as Classifiers" R6 Wonchan Lee, Bow-Yaw Wang and Kwangkeun Yi "Termination Analysis with Algorithmic Learning" R7 Marc Brockschmidt, Richard Musiol, Carsten Otto and Jürgen Giesl "Automated Termination Proofs for Java Programs with Cyclic Data" R8 Javier Esparza, Andreas Gaiser and Stefan Kiefer "Proving Termination of Probabilistic Programs Using Patterns" 3:35 - 4:00: Break 4:00 - 6:05: ABSTRACTION R9 Arnaud Venet "The Gauge Domain: Scalable Analysis of Linear Inequality Invariants" R10 Josh Berdine, Arlen Cox, Samin Ishtiaq and Christoph Wintersteiger "Diagnosing Abstraction Failure for Separation Logic-based Analyses" R11 Aditya Thakur and Thomas Reps "A Method for Symbolic Computation of Abstract Operations" R12 Simone Fulvio Rollini, Ondrej Sery and Natasha Sharygina "Leveraging Interpolant Strength in Model Checking" T3 Evan Driscoll, Aditya Thakur and Thomas Reps "OpenNWA: A Nested Word Automaton Library" T4 Aws Albarghouthi, Yi Li, Arie Gurfinkel and Marsha Chechik "UFO: A Framework for Abstraction- and Interpolation-Based Verification" T5 Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise and Natasha Sharygina "SAFARI: SMT-based Abstraction For Arrays with Interpolants" 6:30 - 8:30: PC dinner Wednesday July 11 ---------------------------------------- 8:35 - 10:35: CONCURRENCY & SOFTWARE VERIFICATION R13 Mohamed Faouzi Atig, Ahmed Bouajjani, Michael Emmi and Akash Lal "Detecting Fair Non-Termination in Multithreaded Programs" R14 Vineet Kahlon and Chao Wang "Lock Removal for Concurrent Trace Programs" R15 Gerhard Schellhorn, John Derrick and Heike Wehrheim "How to prove algorithms linearisable" R16 Anthony Widjaja Lin and Matthew Hague "Synchronisation- and Reversal-Bounded Analysis of Multithreaded Programs with Counters" R17 Alessandro Cimatti and Alberto Griggio "Software Model Checking via IC3" 10:35 - 11:00: Break 11:00 - 12:00: "Model Checking Cell Biology" (David Dill - Keynote) 12:00 - 1:30: Lunch 1:30 - 3:00: BIOLOGY & PROBABILISTIC SYSTEMS R18 Calin Guet, Ashutosh Gupta, Thomas A. Henzinger, Maria Mateescu and Ali Sezgin "Delayed Continuous Time Markov Chains for Genetic Regulatory Circuits" R19 Anvesh Komuravelli, Corina S. Pasareanu and Edmund M. Clarke "Assume-Guarantee Abstraction Refinement for Probabilistic Systems" R20 Cyrille Jegourel, Axel Legay and Sean Sedwards "Cross entropy optimisation of importance sampling parameters for statistical model checking" T6 David Benque, Sam Bourton, Caitlin Cockerton, Byron Cook, Jasmin Fisher, Samin Ishtiaq, Nir Piterman, Alex Taylor and Moshe Vardi "Ripple: Visual Tool for Modeling and Analysis of Biological Networks" T7 Stefan Kiefer, Andrzej Murawski, Joel Ouaknine, Björn Wachter and James Worrell "APEX: An analyzer for open probabilistic programs" 3:30 - 4:00: Break 4:00 - 5:30: *EMBEDDED AND CONTROL SYSTEMS* - special track session R21 Adiya Zutshi, Sriram Sankaranarayanan and Ashish Tiwari "Timed Relational Abstractions For Sampled Data Control Systems" R22 Rupak Majumdar and Majid Zamani "Approximately Bisimilar Symbolic Models for Digital Control Systems" R23 Alessandro Cimatti, Raffaele Corvino, Armando Lazzaro, Iman Narasamdya, Tiziana Rizzo, Marco Roveri, Angela Sanseviero and Andrei Tchaltsev "Formal Verification and Validation of ERTMS Industrial Railway Train Spacing System" T8 Philip Armstrong, Joel Ouaknine, Hristina Palikareva and Bill Roscoe "Recent Developments in FDR" T9 Songzheng Song, Jun Sun, Yang Liu and Jin Song Dong "A Model Checker for Hierarchical Probabilistic Real-time Systems" 6:00 - 9:30: Banquet Thursday July 12 ---------------------------------------- 8:30 - 10:00: *SAT/SMT SOLVING AND SMT-BASED VERIFICATION* - special track session R24 Isil Dillig, Thomas Dillig, Kenneth McMillan and Alex Aiken "Minimum Satisfying Assignments for SMT" R25 Cheng-Shen Han and Jie-Hong Roland Jiang "When Boolean Satisfiability Meets Gaussian Elimination in a Simplex Way" R26 Akash Lal, Shaz Qadeer and Shuvendu Lahiri "Corral: A Solver for Reachability Modulo Theories" T10 Shuvendu Lahiri, Chris Hawblitzel, Ming Kawaguchi and Henrique Rebêlo "SymDiff: A language-agnostic semantic diff tool" T11 Sylvain Conchon, Amit Goel, Sava Krstic, Alain Mebsout and Fatiha Zaidi "Cubicle: A Parallel SMT-based Model Checker for Parameterized Systems" 10:00 - 10:30: Break 10:30 - 12:00: *TIMED & HYBRID SYSTEMS* - special track session R27 Shibashis Guha, Chinmay Narayan and S. Arun-Kumar "On Decidability of Prebisimulation for Timed Automata" R28 Ichiro Hasuo and Kohei Suenaga "Exercises in Nonstandard Static Analysis of Hybrid Systems" R29 Sergiy Bogomolov, Goran Frehse, Radu Grosu, Hamed Ladan, Andreas Podelski and Martin Wehrle "A Box-Based Distance between Regions for Guiding the Reachability Analysis of SpaceEx" T12 Ashish Tiwari "HybridSal Relational Abstracter" T13 Swarat Chaudhuri and Armando Solar-Lezama "Euler: A System for Numerical Optimization of Programs" 12:00 - 1:30: Lunch 1:30 - 2:45: *HARDWARE VERIFICATION* - special track session R30 Sela Mador-Haim, Luc Maranget, Susmit Sarkar, Scott Owens, Jade Alglave, Kayvan Memarian, Rajeev Alur, Milo Martin, Peter Sewell and Derek Williams "An Axiomatic Memory Model for Power Multiprocessors" R31 Flavio M de Paula, Alan Hu and Amir Nahir "nuTAB-BackSpace: Rewriting to Normalize Non-Determinism in Post-Silicon Debug Traces" R32 Zyad Hassan, Aaron Bradley and Fabio Somenzi "Incremental Inductive CTL Model Checking" 2:45 - 3:35: Miscellaneous Tools T14 Rishabh Singh and Armando Solar-Lezama "SPT : Storyboard Programming Tool" T15 Patrick Rondon, Ming Kawaguchi, Alexander Bakst and Ranjit Jhala "CSolve: Verifying C With Liquid Types" T16 Daniel Schwartz-Narbonne, Feng Liu, David August and Sharad Malik "PASSERT: A tool for debugging parallel programs" T17 Joxan Jaffar, Vijayaraghavan Murali, Jorge A. Navas and Andrew E. Santosa "TRACER: A Symbolic Execution Tool for Verification" T18 Stephan Arlt and Martin Schäf "Joogie: Infeasible Code Detection for Java" T19 David Hopkins, Andrzej Murawski and Luke Ong "Hector: An Equivalence Checker for a Higher-Order Fragment of ML" T20 Jan Hoffmann, Klaus Aehlig and Martin Hofmann "Resource Aware ML" 3:35 - 4:00: Break 4:00 - 5:30: Tool demo/poster session 5:30 - 6:30: CAV business meeting 6:30 - 9:00: SC dinner Friday July 13 ---------------------------------------- 9:00 - 10:00: On security of voting machines (Alex Haldermann - Invited talk) 10:00 - 10:30: Break 10:30 - 11:45: *SECURITY* - special track session R33 Matt Fredrikson, Richard Joiner, Somesh Jha, Thomas Reps, Phillip Porras, Hassen Saidi and Vinod Yegneswaran "Efficient Runtime Policy Enforcement Using Counterexample-Guided Abstraction Refinement" R34 Boris Köpf, Laurent Mauborgne and Martín Ochoa "Automatic Quantification of Cache Side-Channels" R35 William Harris, Somesh Jha and Thomas Reps "Secure Programming via Visibly Pushdown Safety Games" 11:45 - 11:50: Mini-break 11:50 - 1:05: VERIFICATION AND SYNTHESIS R36 Nishant Sinha, Nimit Singhania, Satish Chandra and Manu Sridharan "Alternate and Learn: Finding witnesses without looking all over" R37 Duc Hiep Chu and Joxan Jaffar "A Complete Method for Symmetry Reduction in Safety Verification" R38 Rishabh Singh and Sumit Gulwani "Synthesizing Number Transformations from Input-Output Examples" 1:00 - 1:15: Conference Wrap-up

1 0

ANNOUNCE: forthcoming O'Reilly book on Parallel and Concurrent Haskell
by Simon Marlow 17 May '12

17 May '12

I'm delighted to announce that O'Reilly have agreed to publish a book on Parallel and Concurrent Haskell authored by me. The plan is to make a significantly revised and extended version of the Parallel and Concurrent Haskell tutorial from CEFP'11: http://community.haskell.org/~simonmar/bib/par-tutorial-cefp-2012_abstract.… The book will be published in both hardcopy and electronic formats, and will also be available online under a Creative Commons license (Attribution-NonCommercial-NoDerivs 3.0). There will be some mechanism for people to see and comment on early drafts, but I don't know the details yet. When will it be done? I can't say for sure, but the tentative date for completion is March 2013. I'm really keen for this to be a book that will be useful to people both learning about parallelism and concurrency in Haskell, and coding stuff for real-world use. If there are topics or application areas that you'd like to see covered, or any other suggestions, please let me know. All contributions will be acknowledged, of course! Cheers, Simon

4 3

Haskell Weekly News: Issue 227
by Daniel Santa Cruz 17 May '12

17 May '12

Welcome to issue 227 of the HWN, an issue covering crowd-sourced bits of information about Haskell from around the web. This issue covers the week of May 6 to 12, 2012. Announcements Doaitse Swierstra reminded us about the Summer School on Applied Functional Programming, at Utrech University. Hurry to check it out, as the deadline for registration is May 20th! [1] http://goo.gl/TZYdd Janis Voigtlander announced the release of the 22nd edition of the Haskell Communities and Activities Report. [2] http://goo.gl/pXIZn Quotes of the Week * dcoutts: (on #darcs): "[on github:] it's like the facebook of source repos" * dmwit: "Functional programming" is a technical term that means more than just what the two words mean separately. * Axman6: "GHC Warning: Did you see that in an OOP textbook? You probably don't want to be doing that" * StevenKaas: Haskell's Wager: what if infinite lists can suffer infinitely even when lazily evaluated? * quicksilver: "Patent covering a device for emitting greetings to the world community as a whole in computer-readable format" (US Patent no 1787528391) Top Reddit Stories * Videos to the functional programming course I attend are freely available. I thought you might enjoy them. Domain: self.haskell, Score: 47, Comments: 10 On Reddit: [3] http://goo.gl/SoV7x Original: [4] http://goo.gl/SoV7x * red-black trees in haskell, using GADTs, existential types, and zippers, oh my Domain: gist.github.com, Score: 40, Comments: 21 On Reddit: [5] http://goo.gl/Ae08L Original: [6] http://goo.gl/iDxjY * Equality proofs and deferred type errors, A compiler pearl [Vytiniotis, Peyton Jones,Magalhaes PDF] Domain: research.microsoft.com, Score: 40, Comments: 17 On Reddit: [7] http://goo.gl/6OUbX Original: [8] http://goo.gl/OP6ep * LLVM now supports NVIDIA GPU's Domain: nvidianews.nvidia.com, Score: 36, Comments: 19 On Reddit: [9] http://goo.gl/DF7sY Original: [10] http://goo.gl/rvYdL * The Architecture of Open Source Applications, Volume II (with chapters on GHC and Yesod, royalties go to Amnesty International) Domain: lulu.com, Score: 35, Comments: 9 On Reddit: [11] http://goo.gl/XfsXB Original: [12] http://goo.gl/1sr6u * Jesper's Blog: My Take on Haskell vs Scala Domain: jnordenberg.blogspot.com, Score: 29, Comments: 8 On Reddit: [13] http://goo.gl/3EM45 Original: [14] http://goo.gl/aWGgn * Haskell Communities and Activities Report --- May 2012 Domain: haskell.org, Score: 27, Comments: 3 On Reddit: [15] http://goo.gl/q8XFZ Original: [16] http://goo.gl/fW3Sf * Keter: Web App Deployment Domain: yesodweb.com, Score: 23, Comments: 19 On Reddit: [17] http://goo.gl/VOSVF Original: [18] http://goo.gl/OJ783 * A small and simple tip for Google Code Jam-mers Domain: self.haskell, Score: 22, Comments: 15 On Reddit: [19] http://goo.gl/9QPDW Original: [20] http://goo.gl/9QPDW * Composable Value Editors for GTK Domain: twdkz.wordpress.com, Score: 21, Comments: On Reddit: [21] http://goo.gl/w4WoR Original: [22] http://goo.gl/LevtB * The Brittleness of Type Hierarchies (codegrunt.co.uk) and a Haskell approach Domain: self.haskell, Score: 16, Comments: 17 On Reddit: [23] http://goo.gl/w4m8o Original: [24] http://goo.gl/w4m8o Top StackOverflow Questions * Static types, polymorphism and specialization votes: 18, answers: 3 Read on SO: [25] http://goo.gl/wxDZt * Redoing the standard classes [closed] votes: 12, answers: 2 Read on SO: [26] http://goo.gl/22MCG * Using Cont to acquire values from the future and the past votes: 11, answers: 1 Read on SO: [27] http://goo.gl/1zSVo * Why is `($ 4) (> 3)` equivalent to `4 > 3`? votes: 9, answers: 3 Read on SO: [28] http://goo.gl/5oTei * Recursively defined instances and constraints votes: 9, answers: 1 Read on SO: [29] http://goo.gl/uliWA * Freeing memory allocated with newCString votes: 8, answers: 1 Read on SO: [30] http://goo.gl/k3Izw * What is the meaning of “quasi” in quasiquotations? votes: 8, answers: 5 Read on SO: [31] http://goo.gl/YjPbl * Ensuring files are closed promptly votes: 7, answers: 3 Read on SO: [32] http://goo.gl/UCKSB * Is there ever a good reason to use unsafePerformIO? votes: 7, answers: 5 Read on SO: [33] http://goo.gl/y2meC * What characters are permitted for haskell operators? votes: 7, answers: 3 Read on SO: [34] http://goo.gl/0n1kX * Defining an algebra module using constructive-algebra package votes: 6, answers: 2 Read on SO: [35] http://goo.gl/vqIcG * Haskell: Type safety with logically different Boolean values votes: 6, answers: 3 Read on SO: [36] http://goo.gl/f1Gtz * Data structure to represent automata votes: 5, answers: 2 Read on SO: [37] http://goo.gl/MhsvC Until next time, Daniel Santa Cruz References 1. http://permalink.gmane.org/gmane.comp.lang.haskell.cafe/98235 2. http://permalink.gmane.org/gmane.comp.lang.haskell.general/19294 3. http://www.reddit.com/r/haskell/comments/tgz57/videos_to_the_functional_pro… 4. http://www.reddit.com/r/haskell/comments/tgz57/videos_to_the_functional_pro… 5. https://gist.github.com/2659812 6. http://www.reddit.com/r/haskell/comments/ti5il/redblack_trees_in_haskell_us… 7. http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/icfp12.p… 8. http://www.reddit.com/r/haskell/comments/tjnzj/equality_proofs_and_deferred… 9. http://nvidianews.nvidia.com/Releases/NVIDIA-Contributes-CUDA-Compiler-to-O… 10. http://www.reddit.com/r/haskell/comments/tgdia/llvm_now_supports_nvidia_gpu… 11. http://www.lulu.com/shop/amy-brown-and-greg-wilson/the-architecture-of-open… 12. http://www.reddit.com/r/haskell/comments/teqai/the_architecture_of_open_sou… 13. http://jnordenberg.blogspot.com/2012/05/my-take-on-haskell-vs-scala.html 14. http://www.reddit.com/r/haskell/comments/tedrh/jespers_blog_my_take_on_hask… 15. http://www.haskell.org/communities/05-2012/html/report.html 16. http://www.reddit.com/r/haskell/comments/tivjx/haskell_communities_and_acti… 17. http://www.yesodweb.com/blog/2012/05/keter-app-deployment 18. http://www.reddit.com/r/haskell/comments/thygx/keter_web_app_deployment/ 19. http://www.reddit.com/r/haskell/comments/ta5lx/a_small_and_simple_tip_for_g… 20. http://www.reddit.com/r/haskell/comments/ta5lx/a_small_and_simple_tip_for_g… 21. http://twdkz.wordpress.com/2012/05/10/composable-value-editors/ 22. http://www.reddit.com/r/haskell/comments/tg58a/composable_value_editors_for… 23. http://www.reddit.com/r/haskell/comments/tdmt5/the_brittleness_of_type_hier… 24. http://www.reddit.com/r/haskell/comments/tdmt5/the_brittleness_of_type_hier… 25. http://stackoverflow.com/questions/10534744/static-types-polymorphism-and-s… 26. http://stackoverflow.com/questions/10500320/redoing-the-standard-classes 27. http://stackoverflow.com/questions/10560124/using-cont-to-acquire-values-fr… 28. http://stackoverflow.com/questions/10476883/why-is-4-3-equivalent-to-4-3 29. http://stackoverflow.com/questions/10529360/recursively-defined-instances-a… 30. http://stackoverflow.com/questions/10513007/freeing-memory-allocated-with-n… 31. http://stackoverflow.com/questions/10556631/what-is-the-meaning-of-quasi-in… 32. http://stackoverflow.com/questions/10518049/ensuring-files-are-closed-promp… 33. http://stackoverflow.com/questions/10529284/is-there-ever-a-good-reason-to-… 34. http://stackoverflow.com/questions/10548170/what-characters-are-permitted-f… 35. http://stackoverflow.com/questions/10536990/defining-an-algebra-module-usin… 36. http://stackoverflow.com/questions/10544984/haskell-type-safety-with-logica… 37. http://stackoverflow.com/questions/10516603/data-structure-to-represent-aut…

1 0

Haskell Symposium 2012 - deadline approaching
by Janis Voigtländer 16 May '12

16 May '12

[Deadline for submission of abstracts is in two weeks. The submission page is open, earlier submissions welcome.] ======================================================================== "Haskell 2012" ACM SIGPLAN Haskell Symposium 2012 Copenhagen, Denmark 13th September, 2012 (directly after ICFP) CALL FOR PAPERS http://www.haskell.org/haskell-symposium/2012/ ======================================================================== The ACM SIGPLAN Haskell Symposium 2012 will be co-located with the 2012 International Conference on Functional Programming (ICFP), in Copenhagen, Denmark. The purpose of the Haskell Symposium is to discuss experiences with Haskell and future developments for the language. Topics of interest include, but are not limited to: * Language Design, with a focus on possible extensions and modifications of Haskell as well as critical discussions of the status quo; * Theory, such as formal treatments of the semantics of the present language or future extensions, type systems, and foundations for program analysis and transformation; * Implementations, including program analysis and transformation, static and dynamic compilation for sequential, parallel, and distributed architectures, memory management as well as foreign function and component interfaces; * Tools, in the form of profilers, tracers, debuggers, pre-processors, testing tools, and suchlike; * Applications, using Haskell for scientific and symbolic computing, database, multimedia, telecom and web applications, and so forth; * Functional Pearls, being elegant, instructive examples of using Haskell; * Experience Reports, general practice and experience with Haskell, e.g., in an education or industry context. Papers in the latter three categories need not necessarily report original research results; they may instead, for example, report practical experience that will be useful to others, reusable programming idioms, or elegant new ways of approaching a problem. (Links with more advice appear on the symposium web page.) The key criterion for such a paper is that it makes a contribution from which other Haskellers can benefit. It is not enough simply to describe a program! Regular papers should explain their research contributions in both general and technical terms, identifying what has been accomplished, explaining why it is significant, and relating it to previous work (also for other languages where appropriate). In addition, we solicit proposals for system demonstrations, based on running (perhaps prototype) software rather than necessarily on novel research results. Such short demo proposals should explain why a demonstration would be of interest to the Haskell community. Travel Support: =============== Student attendees with accepted papers can apply for a SIGPLAN PAC grant to help cover travel expenses. PAC also offers other support, such as for child-care expenses during the meeting or for travel costs for companions of SIGPLAN members with physical disabilities, as well as for travel from locations outside of North America and Europe. For details on the PAC programme, see its web page (http://www.sigplan.org/PAC.htm) Proceedings: ============ There will be formal proceedings published by ACM Press. In addition to printed proceedings, accepted papers will be included in the ACM Digital Library. Authors must transfer copyright to ACM upon acceptance (for government work, to the extent transferable), but retain various rights (http://www.acm.org/publications/policies/copyright_policy) Authors are encouraged to publish auxiliary material with their paper (source code, test data, etc.); they retain copyright of auxiliary material. Accepted demo proposals, assessed for relevance by the PC, will be published on the symposium web page, but not formally published in the proceedings. Submission Details: =================== * Abstract Submission: Thu 31st May 2012 * Paper Submission : Sat 2nd June 2012, anywhere on earth * Author Notification: Wed 27th June 2012 * Final Papers Due : Tue 10th July 2012 Submitted papers should be in portable document format (PDF), formatted using the ACM SIGPLAN style guidelines (9pt format, more details appear on the symposium web page). The length is restricted to 12 pages, except for "Experience Report" papers, which are restricted to 6 pages. Each paper submission must adhere to SIGPLAN's republication policy, as explained on the web. Demo proposals are limited to 2-page abstracts, in the same format. "Functional Pearls", "Experience Reports", and "Demo Proposals" should be marked as such with those words in the title at time of submission. The paper submission deadline and length limitations are firm. There will be no extensions, and papers violating the length limitations will be summarily rejected. Submission is via EasyChair: https://www.easychair.org/conferences/?conf=haskell2012 Programme Committee: ==================== * Amal Ahmed, Northeastern University * Jost Berthold, University of Copenhagen * Nils Anders Danielsson, University of Gothenburg * Iavor Diatchki, Galois Inc. * Jeremy Gibbons, University of Oxford * Jurriaan Hage, Utrecht University * Zhenjiang Hu, National Institute of Informatics Tokyo * Daan Leijen, Microsoft Research * Ben Lippmeier, University of New South Wales * Simon Peyton Jones, Microsoft Research * Colin Runciman, University of York * Eijiro Sumii, Tohoku University * Janis Voigtländer (chair), University of Bonn * Brent Yorgey, University of Pennsylvania Links: ====== * http://www.haskell.org/haskell-symposium (the permanent web page of the Haskell Symposium) * http://www.haskell.org/haskell-symposium/2012 (the 2012 Haskell Symposium web page) * http://www.icfpconference.org/icfp2012 (the ICFP 2012 web page)

1 0

HOPE 2012 (a new workshop co-located with ICFP): Call for Talk Proposals
by Amal Ahmed 16 May '12

16 May '12

CALL FOR TALK PROPOSALS HOPE 2012 The 1st ACM SIGPLAN Workshop on Higher-Order Programming with Effects September 9, 2012 Copenhagen, Denmark (the day before ICFP 2012) http://hope2012.mpi-sws.org HOPE is a *new workshop* that is intended to bring together researchers interested in the design, semantics, implementation, and verification of higher-order effectful programs. It will be *informal*, consisting of invited talks, contributed talks on work in progress, and open-ended discussion sessions. This 1st edition of HOPE is dedicated to John Reynolds, whose work is an inspiration to us all. --------------------- Goals of the Workshop --------------------- A recurring theme in many papers at ICFP, and in the research of many ICFP attendees, is the interaction of higher-order programming with various kinds of effects: storage effects, I/O, control effects, concurrency, etc. While effects are of critical importance in many applications, they also make it hard to build, maintain, and reason about one's code. Higher-order languages (both functional and object-oriented) provide a variety of abstraction mechanisms to help "tame" or "encapsulate" effects (e.g. monads, ADTs, ownership types, typestate, first-class events, transactions, Hoare Type Theory, session types, substructural and region-based type systems), and a number of different semantic models and verification technologies have been developed in order to codify and exploit the benefits of this encapsulation (e.g. bisimulations, step-indexed Kripke logical relations, higher-order separation logic, game semantics, various modal logics). But there remain many open problems, and the field is highly active. The goal of the HOPE workshop is to bring researchers from a variety of different backgrounds and perspectives together to exchange new and exciting ideas concerning the design, semantics, implementation, and verification of higher-order effectful programs. We want HOPE to be as informal and interactive as possible. The program will thus involve a combination of invited talks, contributed talks about work in progress, and open-ended discussion sessions. There will be no published proceedings, but participants will be invited to submit working documents, talk slides, etc. to be posted on this website. ----------------------- Call for Talk Proposals ----------------------- We solicit proposals for contributed talks. Proposals should be at most 2 pages, in either plain text or PDF format, and should specify how long a talk the speaker wishes to give. By default, contributed talks will be 30 minutes long, but proposals for shorter or longer talks will also be considered. Speakers may also submit supplementary material (e.g. a full paper, talk slides) if they desire, which PC members are free (but not expected) to read. We are interested in talks on all topics related to the interaction of higher-order programming and computational effects. Talks about work in progress are particularly encouraged. If you have any questions about the relevance of a particular topic, please contact the PC chairs at the address hope2012(a)mpi-sws.org. Deadline for talk proposals: June 8, 2012 (Friday) Notification of acceptance: July 1, 2012 (Sunday) Workshop: September 9, 2012 (Sunday) The submission website is now open: http://www.easychair.org/conferences/?conf=hope2012 --------------------- Workshop Organization --------------------- Program Co-Chairs: Amal Ahmed (Northeastern University) Derek Dreyer (MPI-SWS, Germany) Program Committee: Jim Laird (University of Bath) Rasmus Møgelberg (IT University of Copenhagen) Greg Morrisett (Harvard University) Aleks Nanevski (IMDEA Software Institute) David Naumann (Stevens Institute of Technology) Matthew Parkinson (Microsoft Research Cambridge) François Pottier (INRIA Rocquencourt) Amr Sabry (Indiana University) Eijiro Sumii (Tohoku University) Nikhil Swamy (Microsoft Research Redmond) Nobuko Yoshida (Imperial College London)

1 0

Call for AusHac 2012
by Ivan Lazar Miljenovic 16 May '12

16 May '12

For any Australian Haskellers (or indeed anyone that feels willing to come from wherever you may hail) who have _not_ yet received an email, seen it on Reddit or Google+ but is interested in attending AusHac 2012, we are currently trying to determine which weekend in July best suits everyone. So if you're interested in coming, please fill out the form at http://tinyurl.com/AusHac2012PreferredDates This year we're going to hold AusHac in central Sydney (thanks to Atlassian putting their offices at our disposal!) rather than UNSW, which should make transport and accommodation easier for people. AusHac is open to anyone interested in Haskell, from a complete newbie to one of the Simons. We don't have any specific themes or projects to work on; instead just come along and hack on whatever takes your fancy. -- Ivan Lazar Miljenovic Ivan.Miljenovic(a)gmail.com http://IvanMiljenovic.wordpress.com

1 0