- Haskell - Haskell.org

ICFP 2014 Final Call for Participation
by David Van Horn 01 Aug '14

01 Aug '14

[ Early registration ends 3 Aug; Invited speakers and conference program have been announced. ] ===================================================================== Final Call for Participation ICFP 2014 19th ACM SIGPLAN International Conference on Functional Programming and affiliated events August 31 - September 6, 2014 Gothenburg, Swedenhttp://icfpconference.org/icfp2014/ ===================================================================== ICFP provides a forum for researchers and developers to hear about the latest work on the design, implementations, principles, and uses of functional programming. The conference covers the entire spectrum of work, from practice to theory, including its peripheries. A full week dedicated to functional programming: 1 conference, 1 symposium, 10 workshops, tutorials, programming contest results, student research competition * Program: http://icfpconference.org/icfp2014/program.html * Accepted Papers: http://icfpconference.org/icfp2014/accepted.html * Local arrangements (including travel and accommodation): http://icfpconference.org/icfp2014/local.html * Registration is available via: https://regmaster4.com/2014conf/ICFP14/register.php Early registration is due 3 August, 2014. * Programming contest, 25-28 July, 2014: http://icfpcontest.org/ * Follow @icfp_conference on twitter for the latest news: http://twitter.com/#!/icfp_conference Keynote speakers: * Kathleen Fisher (Tufts University): Using Formal Methods to Enable More Secure Vehicles: DARPA's HACMS Program * Robert Bruce Findler (Northwestern University): Behavioral Software Contracts * Stephanie Weirich (University of Pennsylvania): Depending on Types There are several events affiliated with ICFP: Sunday, August 31 ACM SIGPLAN Workshop on Generic Programming ACM SIGPLAN Workshop on Higher-order Programming with Effects Monday, September 1 – Wednesday, September 3 ICFP Thursday, September 4 ACM SIGPLAN Commercial Users of Functional Programming: Day 1, Tutorials ACM SIGPLAN Haskell Symposium: Day 1 ACM SIGPLAN Workshop on Functional High-Performance Computing ACM SIGPLAN ML Family Workshop Friday, September 5 ACM SIGPLAN Commercial Users of Functional Programming: Day 2, Tutorials ACM SIGPLAN Haskell Symposium: Day 2 ACM SIGPLAN OCaml Workshop ACM SIGPLAN Erlang Workshop Saturday, September 6 ACM SIGPLAN Commercial Users of Functional Programming: Day 3, Talks ACM SIGPLAN Haskell Implementors Workshop ACM SIGPLAN Workshop on Functional Art, Music, Modeling and Design Conference Organizers General Chair: Johan Jeuring, Utrecht University Program Chair: Manuel Chakravarty, University of New South Wales Local Arrangements Chair: Björn von Sydow, Chalmers University Industrial Relations Chair: Anil Madhavapeddy, University of Cambridge Workshop Co-Chairs: Tom Schrijvers, Ghent University Sam Tobin-Hochstadt, Indiana University Programming Contest Co-Chairs: Duncan Coutts, Well Typed LLP Nicolas Wu, University of Oxford Student Research Competition Chair: Meng Wang, Chalmers University Publicity Chair: David Van Horn, University of Maryland Video Chair: Iavor Diatchki, Galois Malcolm Wallace, Standard Chartered Bank Industrial partners: Platinum partners Jane Street Capital Gold partners Google Microsoft Research Mozilla Oracle Labs Standard Chartered Bank Silver partners Bloomberg Credit Suisse CyberPoint Erlang Solutions Facebook Galois Klarna Lexifi Twitter Bronze partners Alephcloud IntelliFactory Opera Software QuviQ Systeor Vest AS =====================================================================

1 0

Haskell Platform 2014.2.0.0 Release Candidate 3
by Mark Lentczner 31 Jul '14

31 Jul '14

Small update to the Haskell Platfrom 2014.2.0.0 release: We have new Release Candidate 3 versions of the source tarball... and a new generic-linux bindist of the platform! - source tarball: haskell-platform-2014.2.0.0-srcdist-RC3.tar.gz <http://www.ozonehouse.com/mark/platform/haskell-platform-2014.2.0.0-srcdist…> - generic linux: haskell-platform-2014.2.0.0-unknown-linux-x86_64-RC3.tar.gz <http://www.ozonehouse.com/mark/platform/haskell-platform-2014.2.0.0-unknown…> *Windows and OS X users: There are no RC3 versions - as the RC2 versions seem to be holding up fine!* *General* - hptool (and hence ./platform.sh script) take a new --prefix parameter that is used for generic (non-OS X, non-Windows) builds: It sets the root under which haskell installations are located. Defaults to /usr/local/haskell. Everything will be placed in a directory named ghc-7.8.3-<arch> under this prefix. - activate-hs script for default Posix-like builds - small fixes to allow bootstrapping the platform with GHC 7.4 - README and LICENSE updated *Source Tarball* - all missing pieces now present - build platfrom from source tarball verified *Generic Linux Binary Dist* - Built from the GHC's generic Linux bindist for Deb 7 style systems - Complete tarball: this is all you need to install Haskell on a compatible system - Built on Ubuntu 12.04LTS - Tested on Ubuntu 14 - my system needed a symlink from libgmp.so to libgmp.so.10 - this seems to be an issue with the GHC bindist built components To install this: cd / sudo tar xvf ~/haskell-platform-2014.2.0.0-unknown-linux-x86_64-RC3.tar.gz sudo /usr/local/haskell/ghc-7.8.3-x8_64/bin/activate-hs This will finish the package registration, and install symlinks from /usr/local/bin for all the standard haskell command line tools. — Mark *shasum -a 256:* ab759ec50618f2604163eca7ad07e50c8292398a2d043fdc1012df161b2eb89a haskell-platform-2014.2.0.0-srcdist-RC3.tar.gz 0da6879ae657481849e7ec4e5d3c4c035e090824167f97434b48af297ec17cf9 haskell-platform-2014.2.0.0-unknown-linux-x86_64-RC3.tar.gz

1 0

Haskell Weekly News: Issue 300
by Daniel Santa Cruz 31 Jul '14

31 Jul '14

Welcome to issue 300 of the HWN, an issue covering crowd-sourced bits of information about Haskell from around the web. This issue covers from July 13 to 26, 2014 Looks like we are chuck-full of goodies this time around! Enjoy! Quotes of the Week * Cale: Functions aren't monads, the type constructor (->) e is a monad * glguy: There's no achievement for using all the operators * benmachine: adoption by lots of people may stunt progress of haskell, but it will probably help the progress of people Top Reddit Stories * Somehow, this happened. Haskell Ryan Gosling. Domain: haskellryangosling.tumblr.com, Score: 144, Comments: 31 Original: [1] http://goo.gl/IQ2f3s On Reddit: [2] http://goo.gl/H24aRa * Papers every haskeller should read Domain: self.haskell, Score: 104, Comments: 35 Original: [3] http://goo.gl/R7uGSB On Reddit: [4] http://goo.gl/R7uGSB * Strict Language Pragma Proposal Domain: ghc.haskell.org, Score: 86, Comments: 95 Original: [5] http://goo.gl/Yq28yt On Reddit: [6] http://goo.gl/BlmXpA * Announcing engine-io and socket-io for Haskell Domain: ocharles.org.uk, Score: 81, Comments: 7 Original: [7] http://goo.gl/PGW8Y8 On Reddit: [8] http://goo.gl/IsGRGi * The Haskell Cast #8 - Ollie Charles on 24 Days of Hackage and Nix Domain: haskellcast.com, Score: 70, Comments: 12 Original: [9] http://goo.gl/jBc9bk On Reddit: [10] http://goo.gl/syhwPd * Blazing Fast HTML - Virtual DOM in Elm Domain: elm-lang.org, Score: 60, Comments: 28 Original: [11] http://goo.gl/3luwtw On Reddit: [12] http://goo.gl/88zNkZ * Idris 0.9.14 released, with updated JavaScript backend, quasiquotes, and lots of internal cleanups and improvements Domain: idris-lang.org, Score: 55, Comments: 11 Original: [13] http://goo.gl/wmW3RM On Reddit: [14] http://goo.gl/fN28z6 * hoodle 0.3 released - free pen note taking program Domain: ianwookim.org, Score: 53, Comments: 15 Original: [15] http://goo.gl/jauFC On Reddit: [16] http://goo.gl/upMnf6 * This just in, from my local GHC/Cabal checkout... (re: Cabal Hell) Domain: self.haskell, Score: 52, Comments: 13 Original: [17] http://goo.gl/tD2yOg On Reddit: [18] http://goo.gl/tD2yOg * Haskell for all: Equational reasoning at scale Domain: haskellforall.com, Score: 52, Comments: 29 Original: [19] http://goo.gl/BZtZ4R On Reddit: [20] http://goo.gl/xKxCM3 * Complete roadmap from total novice to Haskell mastery? Domain: self.haskell, Score: 50, Comments: 74 Original: [21] http://goo.gl/5y1lXA On Reddit: [22] http://goo.gl/5y1lXA * Write webservices around databases with 0 boilerplate: announcing servant 0.1 Domain: alpmestan.com, Score: 50, Comments: 16 Original: [23] http://goo.gl/vzz8aT On Reddit: [24] http://goo.gl/qTty6u * Mutable Algorithms in Immutable Languages, Part 3 Domain: tel.github.io, Score: 49, Comments: 2 Original: [25] http://goo.gl/uG5Bds On Reddit: [26] http://goo.gl/qrdk6Y * Best Practices for Avoiding Cabal Hell Domain: softwaresimply.blogspot.com, Score: 47, Comments: 13 Original: [27] http://goo.gl/OqG241 On Reddit: [28] http://goo.gl/fapyz2 * Applicative (Make) vs Monadic (Shake) build systems Domain: neilmitchell.blogspot.co.uk, Score: 47, Comments: 7 Original: [29] http://goo.gl/CPyzpd On Reddit: [30] http://goo.gl/2eW8Ed * Nemnem - Haskell source hyperlinker Domain: robinp.github.io, Score: 41, Comments: 33 Original: [31] http://goo.gl/2msbLR On Reddit: [32] http://goo.gl/R6hBOl * Let me tell you about the types of data Domain: tel.github.io, Score: 41, Comments: 51 Original: [33] http://goo.gl/ZjJelo On Reddit: [34] http://goo.gl/bbmXSW * Lens Tutorial - Introduction (part 1) Domain: blog.jakubarnold.cz, Score: 39, Comments: 11 Original: [35] http://goo.gl/yQRoPY On Reddit: [36] http://goo.gl/fnbZ0F * Help - I wrote some Haskell code, it works, but it's slower than Python. What did I do wrong? Domain: self.haskell, Score: 39, Comments: 43 Original: [37] http://goo.gl/CG13CR On Reddit: [38] http://goo.gl/CG13CR * IntrinsicSuperclasses for Haskell (new proposal for default superclass instances by Conor McBride) Domain: ghc.haskell.org, Score: 37, Comments: 10 Original: [39] http://goo.gl/vDYUQh On Reddit: [40] http://goo.gl/vZjHXS * hackage-diff: Compare the public API of different versions of a Hackage library Domain: self.haskell, Score: 37, Comments: 32 Original: [41] http://goo.gl/y682CB On Reddit: [42] http://goo.gl/y682CB * How do you avoid the Cabal Hell™? Domain: self.haskell, Score: 36, Comments: 30 Original: [43] http://goo.gl/9uS54H On Reddit: [44] http://goo.gl/9uS54H * Edward Kmett on Hask Domain: youtu.be, Score: 35, Comments: 34 Original: [45] http://goo.gl/1lfywk On Reddit: [46] http://goo.gl/D0AuFQ * Mutable Algorithms in Immutable Languages, Part 2 Domain: tel.github.io, Score: 33, Comments: 1 Original: [47] http://goo.gl/g0ylvT On Reddit: [48] http://goo.gl/jwwr87 * Multi-instance packages status report Domain: permalink.gmane.org, Score: 32, Comments: 7 Original: [49] http://goo.gl/JSPx39 On Reddit: [50] http://goo.gl/2rzPJL * Slides from Conan Elliott's workshop on Denotational Design: from meanings to programs Domain: conal.net, Score: 32, Comments: 6 Original: [51] http://goo.gl/GwO4Fv On Reddit: [52] http://goo.gl/0u9KVl * Reactive-banana anti-tutorial Domain: gelisam.blogspot.ca, Score: 31, Comments: 23 Original: [53] http://goo.gl/D7mv4X On Reddit: [54] http://goo.gl/shMY0N * Intro to Machines & Arrows Part 2: 'Auto' as Category, Applicative & Arrow, ft. locally stateful compositions; Further down the road to an Arrowized FRP implementation. Domain: blog.jle.im, Score: 28, Comments: 9 Original: [55] http://goo.gl/xkwocR On Reddit: [56] http://goo.gl/phqXn8 Top StackOverflow Questions * Examples of histomorphisms in Haskell votes: 16, answers: 2 Read on SO: [57] http://goo.gl/ZmGzI6 * Plan B, or what's the opposite of Maybe's >>=? votes: 15, answers: 2 Read on SO: [58] http://goo.gl/rYWlzQ * Let-renaming function breaks code votes: 14, answers: 2 Read on SO: [59] http://goo.gl/R9CGyL * Pattern matching on rank-2 type votes: 14, answers: 3 Read on SO: [60] http://goo.gl/s0IszK * Haskell algorithm advice and suggestions for alternate solutions votes: 14, answers: 1 Read on SO: [61] http://goo.gl/2l23N8 * Why can't Haskell be tricked into performing IO operations by using strict evaluation? votes: 14, answers: 2 Read on SO: [62] http://goo.gl/Ey9795 * How does lifting (in a functional programming context) relate to category theory? votes: 14, answers: 1 Read on SO: [63] http://goo.gl/esTTbO Until next time, [64]+Daniel Santa Cruz References 1. http://haskellryangosling.tumblr.com/ 2. http://www.reddit.com/r/haskell/comments/2avnc0/somehow_this_happened_haske… 3. http://www.reddit.com/r/haskell/comments/2blsqa/papers_every_haskeller_shou… 4. http://www.reddit.com/r/haskell/comments/2blsqa/papers_every_haskeller_shou… 5. https://ghc.haskell.org/trac/ghc/wiki/StrictPragma 6. http://www.reddit.com/r/haskell/comments/2bi69g/strict_language_pragma_prop… 7. https://ocharles.org.uk/blog/posts/2014-07-13-announcing-socket-io-for-hask… 8. http://www.reddit.com/r/haskell/comments/2aks91/announcing_engineio_and_soc… 9. http://www.haskellcast.com/episode/008-ollie-charles-on-24-days-of-hackage-… 10. http://www.reddit.com/r/haskell/comments/2bbc82/the_haskell_cast_8_ollie_ch… 11. http://elm-lang.org/blog/Blazing-Fast-Html.elm 12. http://www.reddit.com/r/haskell/comments/2bam6p/blazing_fast_html_virtual_d… 13. http://www.idris-lang.org/idris-0-9-14-released/ 14. http://www.reddit.com/r/haskell/comments/2aw6vl/idris_0914_released_with_up… 15. http://ianwookim.org/hoodle/ 16. http://www.reddit.com/r/haskell/comments/2aotln/hoodle_03_released_free_pen… 17. http://www.reddit.com/r/haskell/comments/2b7odl/this_just_in_from_my_local_… 18. http://www.reddit.com/r/haskell/comments/2b7odl/this_just_in_from_my_local_… 19. http://www.haskellforall.com/2014/07/equational-reasoning-at-scale.html 20. http://www.reddit.com/r/haskell/comments/2b7xwx/haskell_for_all_equational_… 21. http://www.reddit.com/r/haskell/comments/2ali12/complete_roadmap_from_total… 22. http://www.reddit.com/r/haskell/comments/2ali12/complete_roadmap_from_total… 23. http://alpmestan.com/posts/2014-07-26-announcing-servant.html 24. http://www.reddit.com/r/haskell/comments/2bs536/write_webservices_around_da… 25. http://tel.github.io/2014/07/15/mutable_algorithms_in_immutable_languages_p… 26. http://www.reddit.com/r/haskell/comments/2ase1q/mutable_algorithms_in_immut… 27. http://softwaresimply.blogspot.com/2014/07/haskell-best-practices-for-avoid… 28. http://www.reddit.com/r/haskell/comments/2ameew/best_practices_for_avoiding… 29. http://neilmitchell.blogspot.co.uk/2014/07/applicative-vs-monadic-build-sys… 30. http://www.reddit.com/r/haskell/comments/2blex3/applicative_make_vs_monadic… 31. http://robinp.github.io/nemnem/ 32. http://www.reddit.com/r/haskell/comments/2ata3n/nemnem_haskell_source_hyper… 33. http://tel.github.io/2014/07/23/types_of_data/ 34. http://www.reddit.com/r/haskell/comments/2bj7it/let_me_tell_you_about_the_t… 35. http://blog.jakubarnold.cz/2014/07/14/lens-tutorial-introduction-part-1.html 36. http://www.reddit.com/r/haskell/comments/2ap02f/lens_tutorial_introduction_… 37. http://www.reddit.com/r/haskell/comments/2brxwp/help_i_wrote_some_haskell_c… 38. http://www.reddit.com/r/haskell/comments/2brxwp/help_i_wrote_some_haskell_c… 39. https://ghc.haskell.org/trac/ghc/wiki/IntrinsicSuperclasses 40. http://www.reddit.com/r/haskell/comments/2avs16/intrinsicsuperclasses_for_h… 41. http://www.reddit.com/r/haskell/comments/2b5jfd/hackagediff_compare_the_pub… 42. http://www.reddit.com/r/haskell/comments/2b5jfd/hackagediff_compare_the_pub… 43. http://www.reddit.com/r/haskell/comments/2al3vx/how_do_you_avoid_the_cabal_… 44. http://www.reddit.com/r/haskell/comments/2al3vx/how_do_you_avoid_the_cabal_… 45. http://youtu.be/Klwkt9oJwg0 46. http://www.reddit.com/r/haskell/comments/2b3rk5/edward_kmett_on_hask/ 47. http://tel.github.io/2014/07/13/mutable_algorithms_in_immutable_languages_p… 48. http://www.reddit.com/r/haskell/comments/2al4cw/mutable_algorithms_in_immut… 49. http://permalink.gmane.org/gmane.comp.lang.haskell.ghc.devel/5413 50. http://www.reddit.com/r/haskell/comments/2bbys6/multiinstance_packages_stat… 51. http://conal.net/talks/lambdajam-2014.pdf 52. http://www.reddit.com/r/haskell/comments/2brioe/slides_from_conan_elliotts_… 53. http://gelisam.blogspot.ca/2014/07/reactive-banana-anti-tutorial.html 54. http://www.reddit.com/r/haskell/comments/2auswf/reactivebanana_antitutorial/ 55. http://blog.jle.im/entry/auto-as-category-applicative-arrow-intro-to-machin… 56. http://www.reddit.com/r/haskell/comments/2aot3i/intro_to_machines_arrows_pa… 57. http://stackoverflow.com/questions/24884475/examples-of-histomorphisms-in-h… 58. http://stackoverflow.com/questions/24902463/plan-b-or-whats-the-opposite-of… 59. http://stackoverflow.com/questions/24724738/let-renaming-function-breaks-co… 60. http://stackoverflow.com/questions/24744294/pattern-matching-on-rank-2-type 61. http://stackoverflow.com/questions/24748750/haskell-algorithm-advice-and-su… 62. http://stackoverflow.com/questions/24775528/why-cant-haskell-be-tricked-int… 63. http://stackoverflow.com/questions/24856963/how-does-lifting-in-a-functiona… 64. https://plus.google.com/105107667630152149014/about

1 0

The ML Family workshop: program and the 2nd call for participation
by oleg＠okmij.org 31 Jul '14

31 Jul '14

Higher-order, Typed, Inferred, Strict: ACM SIGPLAN ML Family Workshop Thursday September 4, 2014, Gothenburg, Sweden Call For Participation and Program http://okmij.org/ftp/ML/ML14.html Early registration deadline is August 3. Please register at https://regmaster4.com/2014conf/ICFP14/register.php The workshop is conducted in close cooperation with the OCaml Users and Developers Workshop http://ocaml.org/meetings/ocaml/2014/ taking place on September 5. *** Program with short summaries *** (The online version links to the full 2-page abstracts) * Welcome 09:00 * Session 1: Module Systems 09:10 - 10:00 1ML -- core and modules as one (Or: F-ing first-class modules) Andreas Rossberg We propose a redesign of ML in which modules are first-class values. Functions, functors, and even type constructors are one and the same construct. Likewise, no distinction is made between structures, records, or tuples, including tuples over types. Yet, 1ML does not depend on dependent types, and its type structure is expressible in terms of plain System F-omega, in a minor variation of our F-ing modules approach. Moreover, it supports (incomplete) Hindley/Milner-style type inference. Both is enabled by a simple universe distinction into small and large types. Type-level module aliases: independent and equal Jacques Garrigue; Leo White We promote the use of type-level module aliases, a trivial extension of the ML module system, which helps avoiding code dependencies, and provides an alternative to strengthening for type equalities. * Session 2: Beyond Hindley-Milner 10:30 - 11:20 The Rust Language and Type System (Demo) Felix Klock; Nicholas Matsakis Rust is a new programming language for developing reliable and efficient systems. It is designed to support concurrency and parallelism in building applications and libraries that take full advantage of modern hardware. Rust's static type system is safe and expressive and provides strong guarantees about isolation, concurrency, and memory safety. Rust also offers a clear performance model, making it easier to predict and reason about program efficiency. One important way it accomplishes this is by allowing fine-grained control over memory representations, with direct support for stack allocation and contiguous record storage. The language balances such controls with the absolute requirement for safety: Rust's type system and runtime guarantee the absence of data races, buffer overflows, stack overflows, and accesses to uninitialized or deallocated memory. In this demonstration, we will briefly review the language features that Rust leverages to accomplish the above goals, focusing in particular on Rust's advanced type system, and then show a collection of concrete examples of program subroutines that are efficient, easy for programmers to reason about, and maintain the above safety property. Doing web-based data analytics with F# (Informed Position) Tomas Petricek; Don Syme With type providers that integrate external data directly into the static type system, F# has become a fantastic language for doing data analysis. Rather than looking at F# features in isolation, this paper takes a holistic view and presents the F# approach through a case study of a simple web-based data analytics platform. * Session 3: Verification 11:40 - 12:30 Well-typed generic smart-fuzzing for APIs (Experience report) Thomas Braibant; Jonathan Protzenko; Gabriel Scherer In spite of recent advances in program certification, testing remains a widely-used component of the software development cycle. Various flavors of testing exist: popular ones include unit testing, which consists in manually crafting test cases for specific parts of the code base, as well as quickcheck-style testing, where instances of a type are automatically generated to serve as test inputs. These classical methods of testing can be thought of as internal testing: the test routines access the internal representation of the data structures to be checked. We propose a new method of external testing where the library only deals with a module interface. The data structures are exported as abstract types; the testing framework behaves like regular client code and combines functions exported by the module to build new elements of the various abstract types. Any counter-examples are then presented to the user. Furthermore, we demonstrate that this methodology applies to the smart-fuzzing of security APIs. Improving the CakeML Verified ML Compiler Ramana Kumar; Magnus O. Myreen; Michael Norrish; Scott Owens The CakeML project comprises a mechanised semantics for a subset of Standard ML and a formally verified compiler. We will discuss our plans for improving and applying CakeML in four directions: optimisations, new primitives, a library, and verified applications. * Session 4: Implicits 14:00 - 14:50 Implicits in Practice (Demo) Nada Amin; Tiark Rompf Popularized by Scala, implicits are a versatile language feature that are receiving attention from the wider PL community. This demo will present common use cases and programming patterns with implicits in Scala. Modular implicits Leo White; Frédéric Bour We propose a system for ad-hoc polymorphism in OCaml based on using modules as type-directed implicit parameters. * Session 5: To the bare metal 15:10 - 16:00 Metaprogramming with ML modules in the MirageOS (Experience report) Anil Madhavapeddy; Thomas Gazagnaire; David Scott; Richard Mortier In this talk, we will go through how MirageOS lets the programmer build modular operating system components using a combination of functors and metaprogramming to ensure portability across both Unix and Xen, while preserving a usable developer workflow. Compiling SML# with LLVM: a Challenge of Implementing ML on a Common Compiler Infrastructure Katsuhiro Ueno; Atsushi Ohori We report on an LLVM backend of SML#. This development provides detailed accounts of implementing functional language functionalities in a common compiler infrastructure developed mainly for imperative languages. We also describe techniques to compile SML#'s elaborated features including separate compilation with polymorphism, and SML#'s unboxed data representation. * Session 6: No longer foreign 16:30 - 18:00 A Simple and Practical Linear Algebra Library Interface with Static Size Checking (Experience report) Akinori Abe; Eijiro Sumii While advanced type systems--specifically, dependent types on natural numbers--can statically ensure consistency among the sizes of collections such as lists and arrays, such type systems generally require non-trivial changes to existing languages and application programs, or tricky type-level programming. We have developed a linear algebra library interface that guarantees consistency (with respect to dimensions) of matrix (and vector) operations by using generative phantom types as fresh identifiers for statically checking the equality of sizes (i.e., dimensions). This interface has three attractive features in particular. (i) It can be implemented only using fairly standard ML types and its module system. Indeed, we implemented the interface in OCaml (without significant extensions like GADTs) as a wrapper for an existing library. (ii) For most high-level operations on matrices (e.g., addition and multiplication), the consistency of sizes is verified statically. (Certain low-level operations, like accesses to elements by indices, need dynamic checks.) (iii) Application programs in a traditional linear algebra library can be easily migrated to our interface. Most of the required changes can be made mechanically. To evaluate the usability of our interface, we ported to it a practical machine learning library (OCaml-GPR) from an existing linear algebra library (Lacaml), thereby ensuring the consistency of sizes. SML3d: 3D Graphics for Standard ML (Demo) John Reppy The SML3d system is a collection of libraries designed to support real-time 3D graphics programming in Standard ML (SML). This paper gives an overview of the system and briefly highlights some of the more interesting aspects of its design and implementation. * Poster presentation, at the joint poster session with the OCaml workshop Nullable Type Inference Michel Mauny; Benoit Vaugon We present a type system for nullable types in an ML-like programming language. We start with a simple system, presented as an algorithm, whose interest is to introduce the formalism that we use. We then extend it as system using subtyping constraints, that accepts more programs. We state the usual properties for both systems. This is work in progress. Program Committee Kenichi Asai Ochanomizu University, Japan Matthew Fluet Rochester Institute of Technology, USA Jacques Garrigue Nagoya University, Japan Dave Herman Mozilla, USA Stefan Holdermans Vector Fabrics, Netherlands Oleg Kiselyov (Chair) University of Tsukuba, Japan Keiko Nakata Tallinn University of Technology, Estonia Didier Remy INRIA Paris-Rocquencourt, France Zhong Shao Yale University, USA Hongwei Xi Boston University, USA

1 0

ETAPS 2015 1st call for papers
by Tarmo Uustalu 29 Jul '14

29 Jul '14

****************************************************************** CALL FOR PAPERS: ETAPS 2015 18th European Joint Conferences on Theory And Practice of Software London, UK, 11-18 April 2015 http://www.etaps.org/2015 ****************************************************************** -- ABOUT ETAPS -- ETAPS is the primary European forum for academic and industrial researchers working on topics relating to software science. ETAPS, established in 1998, is a confederation of six main annual conferences, accompanied by satellite workshops. ETAPS 2015 is the eighteenth event in the series. -- MAIN CONFERENCES (13-17 April) -- * CC: Compiler Construction (PC chair Björn Franke, University of Edinburgh, UK) * ESOP: European Symposium on Programming (PC chair Jan Vitek, Northeastern University, USA) * FASE: Fundamental Approaches to Software Engineering (PC chairs Alexander Egyed, Johannes Kepler U Linz, Austria, and Ina Schaefer, Technische Universität Braunschweig, Germany) * FOSSACS: Foundations of Software Science and Computation Structures (PC chair Andrew Pitts, University of Cambridge, UK) * POST: Principles of Security and Trust (PC chairs Riccardo Focardi, Università Ca' Foscari Venezia, Italy, and Andrew Myers, Cornell University, USA) * TACAS: Tools and Algorithms for the Construction and Analysis of Systems (PC chairs Christel Baier, Technische Univ Dresden, Germany, and Cesare Tinelli, The University of Iowa, USA) TACAS '14 hosts the 4rd Competition on Software Verification (SV-COMP). -- INVITED SPEAKERS -- * Unifying speakers: Robert Harper (Carnegie Mellon University, USA) Catuscia Palamidessi (INRIA Saclay and LIX, France) * CC invited speaker: Keshav Pingali (University of Texas, USA) * FoSSaCS invited speaker: Frank Pfenning (Carnegie Mellon University, USA) * TACAS invited speaker: Wang Yi (Uppsala Universitet, Sweden) -- IMPORTANT DATES -- * 10 October 2014: Submission deadline for abstracts * 17 October 2014: Submission deadline for full papers * 3-5 December 2014: Author response period (ESOP and FoSSaCS only) * 19 December 2014: Notification of acceptance * 16 January 2015: Camera-ready versions due -- SUBMISSION INSTRUCTIONS -- ETAPS conferences accept two types of contributions: research papers and tool demonstration papers. Both types will appear in the proceedings and have presentations during the conference. ESOP and FoSSaCS accept only research papers. TACAS has more paper categories (see http://www.etaps.org/2015/tacas) A condition of submission is that, if the submission is accepted, one of the authors attends the conference to give the presentation. Submitted papers must be in English presenting original research. They must be unpublished and not submitted for publication elsewhere. In particular, simultaneous submission of the same contribution to multiple ETAPS conferences is forbidden. The proceedings will be published in the Advanced Research in Computing and Software Science (ARCoSS) subline of Springer's Lecture Notes in Computer Science series. Papers must follow the formatting guidelines specified by Springer at http://www.springer.de/comp/lncs/authors.html and be submitted electronically in pdf through the EasyChair author interface of the respective conference (HotCRP for ESOP). Submissions not adhering to the specified format and length may be rejected immediately. - Research papers FASE, FOSSACS and TACAS have a page limit of 15 pages for research papers, whereas CC, POST allow at most 20 pages and ESOP 25 pages. Additional material intended for the referees but not for publication in the final version - for example, details of proofs - may be placed in a clearly marked appendix that is not included in the page limit. ETAPS referees are at liberty to ignore appendices and papers must be understandable without them. In addition to regular research papers, TACAS solicits also case study papers (at most 15 pages). Both TACAS and FASE solicit also regular tool papers (at most 15 pages). - Tool demonstration papers Submissions should consist of two parts: * The first part, at most 4 pages, should describe the tool presented. Please include the URL of the tool (if available) and provide information that illustrates the maturity and robustness of the tool. (This part will be included in the proceedings.) * The second part, at most 6 pages, should explain how the demonstration will be carried out and what it will show, including screen dumps and examples. (This part will be not be included in the proceedings, but will be evaluated. ESOP and FOSSACS do not accept tool demonstration papers. TACAS has a page limit of 6 pages for tool demonstrations. -- SATELLITE EVENTS (11-12 April, 18 April) -- Around 20 satellite workshops will take place before and after the main conferences. -- HOST CITY -- London, the capital city of England and the UK, is a leading global city, with strengths in the arts, commerce, education, entertainment, fashion, finance, healthcare, media, professional services, research and development, tourism and transport all contributing to its prominence. It is one of the world's leading financial centers and a world cultural capital. It is the world's most-visited city as measured by international arrivals and has the world's largest city airport system measured by passenger traffic. In 2012, London became the first city to host the modern Summer Olympic Games three times. -- HOST INSTITUTION -- ETAPS 2015 is hosted by the School of Electrical Engineering and Computer Science of the Queen Mary University of London. The main campus is located in the Mile End area of the East End of London. -- ORGANIZERS * General chairs: Pasquale Malacaria, Nikos Tzevelekos * Workshops chair: Paulo Oliva -- FURTHER INFORMATION -- Please do not hesitate to contact the organizers at p.malacaria(a)qmul.ac.uk, nikos.tzevelekos(a)qmul.ac.uk.

1 0

early adopters rejoyce! Haskell Platform 2014.2.0.0 Release Candidate 2
by Mark Lentczner 29 Jul '14

29 Jul '14

The long anticipated Haskell Platform 2014.2 release, including GHC 7.8.3, and numerous updated packages, is almost here! We have created "Release Candidate 2" installers for OS X and Windows, and believe, barring show stopper issues, creepers exploding, or unexpected trips to the nether, these will likely be blessed as the final by the end of the week. If you would like to be an early adopter, please try 'em out... - source tarball: haskell-platform-2014.2.0.0-RC2.tar.gz <http://www.ozonehouse.com/mark/platform/haskell-platform-2014.2.0.0-RC2.tar…> - source repo: haskell/haskell-platform at 2014.2.0.0-RC2 <https://github.com/haskell/haskell-platform/tree/2014.2.0.0-RC2> - windows 32bit: hskellPlatform-2014.2.0.0-i386-RC2-setup.exe <http://www.ozonehouse.com/mark/platform/hskellPlatform-2014.2.0.0-i386-RC2-…> - windows 64bit:hskellPlatform-2014.2.0.0-x86_64-RC2-setup.exe <http://www.ozonehouse.com/mark/platform/hskellPlatform-2014.2.0.0-x86_64-RC…> - os x 64bit: Haskell Platform 2014.2.0.0 64bit RC2.signed.pkg <http://www.ozonehouse.com/mark/platform/Haskell%20Platform%202014.2.0.0%206…> - travis-ci build: haskell/haskell-platform <https://travis-ci.org/haskell/haskell-platform> *Short Notes for RC2, read these if nothing else:* *General* - includes GHC 7.8.3 - includes long awaited updates to OpenGL & GLUT packages - most other packages brought up to date (or nearly so) - website is still woefully out of date... will work on it this week *Windows* *Extra thanks to Randy Polen for burning the midnight-oil to get ths out* - removed unneeded python (et al) files from the GHC bindist for 64-bit Windows (referenced in GHC ticket #9014 <https://ghc.haskell.org/trac/ghc/ticket/9014>) - added HTML "view source" pages for the GHC packages that was missing from the GHC bindist for both 32- and 64-bit Windows. *Mac OS X* *If you installed RC1 or older versions of the platform, you can remove them first with the command *sudo uninstall-hs only 7.8.3 --remove *Run it without *--remove* to see what it will do first, it if you like. You can also just install this one right on top of RC1. If you have older 7.8.3 installs from other distributions (bindist, built from src, etc...) you may want to manually remove them first... YMMV.**. Yoda says: "When doubt you have, the $PATH examine, you must!"* - works on 10.6! and 10.7, 10.8, and 10.9; with gcc or clang based Xcodes - works on 10.10!!! (Yosemite, developer preview 4 release) - works with clang out of the box, and haddock build issues with clang, fixed. *N.B.: If you have hand installed cabal 1.20, please be sure it uses Cabal 1.20.0.2 to fix the haddock issue. The platform on OS X includes cabal 1.18, using 1.18.1.4, which fixes the problem.* *Source tarball* - uses new build machinery... all the kinks may not be worked out, and not all build featuers (notably a --prefix command) are implemented yet. This doesn't affect the content of the Platform, though. - generic *nix builds, and specific distribution builds are forth coming (though feel free to chip in and help!) *Longer Notes for RC2:* *General* - Built with the new shake based build system - cgi package not included as it doesn't build under 7.8, and no word from the maintainer in quite some time - hscolour is included as a tool, mostly as it is used to build the platform itself on win and mac... but technically it isn't part of the platform - the haskell-platform package itself is not in these releases... it never contained anything other than dependencies. *Windows* - The Haskell Platform now provides a native Windows 64-bit installation (haskell-platform issue #54 <https://github.com/haskell/haskell-platform/issues/54>) - All included packages built without --enable-split-objs (GHC 7.8 FAQ <https://ghc.haskell.org/trac/ghc/wiki/GHC-7.8-FAQ#Cabal>) - All included packages built without --enable-shared (GHC ticket #8228 <https://ghc.haskell.org/trac/ghc/ticket/8228>) - If other Haskell Platform installations are detected during the installation of Haskell Platform 2014.2.0.0, a warning is displayed to the user that this is not recommended since problems will arise due to how the PATH is used in many cases to find ancillary build tools - Using ghci to build an executable that links against a DLL may result in numerous warnings about symbols (GHC ticket #9297 <https://ghc.haskell.org/trac/ghc/ticket/9297>) - The Haskell Platform for Windows, both 32-bit and 64-bit, now includes an updated version of the OpenGL Utility Toolkit (GLUT) from the FreeGLUT project, utilizing the pre-built distribution from http://www.transmissionzero.co.uk/software/freeglut-devel/ with the MinGW build (freeglut-MinGW-2.8.1-1.mp.zip). (haskell-platform issue #81 <https://github.com/haskell/haskell-platform/issues/81>) *Mac OS X* - file layout on the Mac has improved. In particular, executables are now installed directly in $prefix/bin dirs, rather than within the package dir - Distributed with a build of 7.8.3 that differs from the released bindist in two ways: a) it was built split-objs for smaller resulting executables, b) it includes Cabal-1.18.1.4 which fixes a particularly nasty problem with haddock, -XCPP, and clang based systems. This ghc-7.8.3 bindist is available as well: - ghc-7.8.3-x86_64-apple-darwin-r3.tar.bz2 <http://www.ozonehouse.com/mark/platform/ghc-7.8.3-x86_64-apple-darwin-r3.ta…> - haddocks finally cross link between packages correctly - includes a new experimental activate-hs command that can switch between multiple installed versions of the platform - includes a slightly updated uninstall-hs command - the cabal command is wrapped to provide a smoother file layout on the Mac... the wrapping only updates the ~/.cabal/config file the first time you run it.. please pay attention to its output - if you have a custom config file, you'll want to update it, as Cabal's defaults have changed *Timetable* - End of this week (from my vacation, I'll point out), we'll declare success and rename the files. — Mark *SHA-256 sums :* 62f39246ad95dd2aed6ece5138f6297f945d2b450f215d074820294310e0c48a Haskell Platform 2014.2.0.0 64bit RC2.signed.pkg 7c7d3585e89e1407461efea29dcaa9628c3be3c47d93a13b5a4978046375e4fd haskell-platform-2014.2.0.0-RC2.tar.gz 6eedd76aafb266d9a09baff80cd2973498ab59195c771f7cd64425d40be29c49 hskellPlatform-2014.2.0.0-i386-RC2-setup.exe b22115ed84d1f7e747d7f0b47e32e1489e4a24613d69c91df4ae32052f88b130 hskellPlatform-2014.2.0.0-x86_64-RC2-setup.exe

1 0

RV 2014: Call for Participation
by Runtime Verification 28 Jul '14

28 Jul '14

****************************************************************** CALL FOR PARTICIPATION RV 2014: 14th International Conference on Runtime Verification September 22 - September 25, 2014, Toronto, Canada http://rv2014.imag.fr ****************************************************************** ***************** OVERVIEW ***************** Runtime verification is concerned with monitoring and analysis of software and hardware system executions. Runtime verification techniques are important for system correctness, reliability, and robustness; they are complementary to conventional testing, and more practical than exhaustive formal verification. Runtime verification can be used prior to deployment, for testing, verification, and debugging purposes, and after deployment for ensuring reliability, safety, and security and for providing fault containment and recovery as well as online system repair. Topics of interest to the conference include: - specification languages - specification mining - program instrumentation - monitor construction techniques - logging, recording, and replay - fault detection, localization, containment, recovery and repair - program steering and adaptation - metrics and statistical information gathering - combination of static and dynamic analyses - program execution visualization - monitoring techniques for safety/mission-critical systems - monitoring distributed systems, cloud services, and big data applications - monitoring security and privacy policies Application areas of runtime verification include safety/mission-critical systems, enterprise and systems software, autonomous and reactive control systems, health management and diagnosis systems, and system security and privacy. ***************** INVITED TALKS ***************** - *Kevin Driscoll* Fellow at Honeywell Labs, USA *Murphy Strikes Again* - *Assaf Schuster* Professor of Computer Science, Computer Science Department, Technion, Israel *Monitoring Big, Distributed, Streaming Data* - *Jeannette Wing* President's Professor of Computer Science, Computer Science Department, Carnegie Mellon University, USA *Formal Methods: An Industrial Perspective* ***************** INVITED TUTORIALS ***************** - *Vijay K. Garg & Neeraj Mittal* UT at Austin & UT at Dallas *A Lattice-Theoretic Approach to Monitoring Distributed Computations* - *David Basin & Felix Klaedtke* ETH-Zurich & NEC Labs, Europe *Runtime Monitoring and Enforcement of Security Policies* ***************** VENUE ***************** The Fields Institute for Research in Mathematical Sciences 222 College Street, Toronto, Ontario, Canada http://www.fields.utoronto.ca/ ***************** REGISTRATION ***************** Registration on line to Aug. 21, on site Sept. 22 Registration fees $575, after Aug. 21 $675 Student $350, after Aug. 21, $450 Fees include proceedings and 1x Conference banquet Additional banquet tickets $80 Registration link: http://www.fields.utoronto.ca/programs/scientific/14-15/RV2014/ ***************** ACCEPTED PAPERS ***************** - Pierre Fraigniaud, Sergio Rajsbaum and Corentin Travers. On the Number of Opinions Needed for Fault-Tolerant Run-Time Monitoring in Distributed Systems - Simon Varvaressos, Kim Lavoie, Sebastien Gaboury and Sylvain Hallé. Multiple Ways to Fail: Generalizing a Monitor's Verdict for the Classification of Execution Traces - Clemens Ballarin. Two Generalisations of Roşu and Chen's Trace Slicing Algorithm A - Martin Hentschel, Richard Bubel and Reiner Hähnle. Symbolic Execution Debugger (SED) - Jiannan Zhai, Nigamanth Sridhar and Jason Hallstrom. Supporting the Specification and Runtime Validation of Asynchronous Calling Patterns in Reactive Systems - Emmanouil Koukoutos and Viktor Kuncak. Checking Data Structure Properties Orders of Magnitude Faster - Maria Christakis, Patrick Emmisberger and Peter Müller. Dynamic Test Generation with Static Fields and Initializers - Aravind Sukumaran-Rajam, Juan Manuel Martinez Caamano, Willy Wolff, Alexandra Jimborean and Philippe Clauss. Speculative Program Parallelization with Scalable and Decentralized Runtime Verification - Christian Colombo and Yliès Falcone. Organising LTL Monitors over Distributed Systems with a Global Clock - Erdal Mutlu, Vladimir Gajinov, Adrian Cristal, Serdar Tasiran and Osman Unsal. Dynamic Verification for Hybrid Concurrent Programming Models - Hsi-Ming Ho, Joel Ouaknine and James Worrell. Online Monitoring of Metric Temporal Logic - David Basin, Germano Caronni, Sarah Ereth, Matúš Harvan, Felix Klaedtke and Heiko Mantel. Scalable Offline Monitoring - David Basin, Felix Klaedtke, Srdjan Marinovic and Eugen Zalinescu. On Real-time Monitoring with Imprecise Timestamps - Anand Yeolekar. Improving dynamic inference with variable dependence graph - Ming Chai and Holger Schlingloff. Monitoring Systems with Extended Live Sequence Charts - Laura Bozzelli and César Sánchez. Foundations of Boolean Stream Runtime Verification - Mitra Tabaei Befrouei, Chao Wang and Georg Weissenbacher. Abstraction and Mining of Traces to Explain Concurrency-Bugs - Stefan Mitsch and André Platzer. ModelPlex: Verified Runtime Validation of Verified Cyber-Physical System Models - Johannes Geist, Kristin Y. Rozier and Johann Schumann. Runtime Observer Pairs and Bayesian Network Reasoners On-board FPGAs: Flight-Certifiable System Health Management for Embedded Systems - Malte Isberner, Falk Howar and Bernhard Steffen The TTT Algorithm: A Redundancy-Free Approach to Active Automata Learning - Kim Lavoie, Corentin Leplongeon, Simon Varvaressos, Sebastien Gaboury and Sylvain Hallé. Portable Runtime Verification with Smartphones and Optical Codes - Adel Dokhanchi, Bardh Hoxha and Georgios Fainekos On-Line Monitoring for Temporal Logic Robustness - Jeff Huang, Cansu Erdogan, Yi Zhang, Brandon Moore, Qingzhou Luo, Aravind Sundaresan and Grigore Rosu. ROSRV: Runtime Verification for Robots - Qingzhou Luo, Yi Zhang, Choonghwan Lee, Dongyun Jin, Patrick Meredith, Traian Serbanuta and Grigore Rosu. RV-Monitor: Efficient Parametric Runtime Verification with Simultaneous Properties - Duc Hiep Chu, Joxan Jaffar and Vijayaraghavan Murali. Lazy Symbolic Execution for Enhanced Learning - Kuei Sun, Daniel Fryer, Ashvin Goel, Dai Qin and Angela Demke Brown. Robust Consistency Checking for Modern Filesystems - Ayoub Nouri, Balaji Raman, Marius Bozga, Axel Legay and Saddek Bensalem. Faster Statistical Model Checking by Means of Abstraction and Learning ***************** CHAIRS AND ORGANIZERS ***************** - General Chair: Sebastian Fischmeister (University of Waterloo, Canada). - PC co-Chairs: - Borzoo Bonakdarpour (McMaster University, Canada) - Scott Smolka (Stony Brook Universtiy, USA) - Tools Track Chair: Ezio Bartocci (TU Vienna, Austria) - Runtime Monitoring Competition Co-Chairs: - Ezio Bartocci (TU Vienna, Austria) - Borzoo Bonakdarpour (McMaster University, Canada) - Ylies Falcone (Université Joseph Fourier, France) - Publicity Chair: Ylies Falcone (Université Joseph Fourier, France) - Local Arrangements Chair: Patrick Lam (University of Waterloo, Canada) ***************** FURTHER INFORMATION ***************** More information about RV2014 is available from the conference web site: http://rv2014.imag.fr

1 0

PPDP 2014: Program and 2nd Call for Participation
by Jacob Johannsen 27 Jul '14

27 Jul '14

====================================================================== CALL FOR PARTICIPATION: PPDP 2014 16th International Symposium on Principles and Practice of Declarative Programming Canterbury, Kent, September 8-10, 2014 http://users-cs.au.dk/danvy/ppdp14/ co-located with LOPSTR 2014 24th International Symposium on Logic-Based Program Synthesis and Transformation Canterbury, Kent, September 9-11, 2014 http://www.iasi.cnr.it/events/lopstr14/ ====================================================================== Two weeks left for early registration (until August 8): http://www.cs.kent.ac.uk/events/2014/ppdp-lopstr-14/ A significant discount is available when registering to both events, especially as a student (until August 8). PPDP 2014 features * an invited talk by Roberto Giacobazzi, shared with LOPSTR: "Obscuring Code -- Unveiling and Veiling Information in Programs" * no fewer than 4 distilled tutorials by - Henrik Nilsson and Ivan Perez: "Declarative Game Programming" - Danko Ilik: "Proofs in Continuation-Passing Style: normalization of Gödel's System T extended with sums and delimited control operators" - Jerzy Karczmarczuk: "On the Declarative Structure of Quantum Concepts: States and Observables" - Ralf Laemmel, Andrei Varanovich, and Martin Leinberger: "Declarative Software Development" * the most influential paper 10-year award for PPDP 2004 Tentative program: ========== Monday 8 September Welcome to PPDP 2014 - 08:45-09:00 Olaf Chitil and Andy King Distilled Tutorial - 9:00-10:00 Ralf Laemmel "Declarative Software Development" Break - 10:00-10:15 Session - 10:15-11:15 10:15-10:45 Rémi Douence and Nicolas Tabareau "Lazier Imperative Programming" 10:45-11:15 Stefan Mehner, Daniel Seidel, Lutz Straßburger and Janis Voigtländer "Parametricity and Proving Free Theorems for Functional-Logic Languages" Break - 11:15-11:30 Session - 11:30-12:30 11:30:-12:00 Paul Tarau "Bijective Collection Encodings and Boolean Operations with Hereditarily Binary Natural Numbers" 12:00-12:30 Flavio Cruz, Ricardo Rocha and Seth Goldstein "Design and implementation of a multithreaded virtual machine for executing linear logic programs" Lunch break - 12:30-14:00 Distilled tutorial - 14:00-15:00 Danko Ilik "Proofs in Continuation-Passing Style: normalization of Gödel's System T extended with sums and delimited control operators" Break - 15:00-15:15 Session - 15:15-16:15 15:15-15:45 Kenichi Asai, Luminous Fennell, Peter Thiemann and Yang Zhang "A Type Theoretic Specification for Partial Evaluation" 15:45-16:15 Paul Downen, Luke Maurer, Zena Ariola and Daniele Varacca "Continuations, Processes, and Sharing" Break - 16:15-16:30 Session - 16:30-17:30 16:30-17:00 Pierre Neron "Partial Inlining for Program Transformation" 17:00-17:30 Jean-Louis Giavitto and José Echeveste "Real-Time Matching of Antescofo Temporal Patterns" Program-chair report - 17:30-17:45 Olivier Danvy ---------- Tuesday 9 September Distilled tutorial - 9:00-10:00 Jerzy Karczmarczuk "On the Declarative Structure of Quantum Concepts: States and Observables" Break - 10:00-10:15 Session - 10:15-11:15 10:15-10:45 José Meseguer and Salvador Lucas "Proving Operational Termination of Declarative Programs in General Logics" 10:45-11:15 Fan Yang, Santiago Escobar, Catherine Meadows, José Meseguer and Paliath Narendran "Theories of Homomorphic Encryption, Unification, and the Finite Variant Property" Break - 11:15-11:30 Session - 11:30-12:30 11:30:-12:00 Tzu-Chun Chen, Mariangiola Dezani-Ciancaglini and Nobuko Yoshida "On the Preciseness of Subtyping in Session Types" 12:00-12:30 Hugo Pacheco, Tao Zan and Zhenjiang Hu "BiFluX: A Bidirectional Functional Update Language for XML" Lunch break - 12:30-14:00 Distilled tutorial - 14:00-15:00 Henrik Nilsson "Declarative Game Programming" Break - 15:00-15:15 Session - 15:15-16:15 15:15-15:45 Francisco Ferreira and Brigitte Pientka "Bidirectional Elaboration of Dependently Typed Programs" 15:45-16:15 Steven Ramsay "Exact Intersection Type Abstractions for Safety Checking of Recursion Schemes" Break - 16:15-16:30 Session - 16:30-17:30 16:30-17:00 Julian Kranz and Axel Simon "Structure-Preserving Compilation: Efficient Integration of Functional DSLs into Legacy Systems" 17:00-17:30 Ulrich Schöpp "Organising Low-Level Programs using Higher Types" ---------- Wednesday 10 September Invited talk - 9:00-10:00 Roberto Giacobazzi Obscuring Code -- Unveiling and Veiling Information in Programs Break - 10:00-10:15 Session - 10:15-11:15 10:15-10:45 Rémy Haemmerlé "On Combining Backward and Forward Chaining in Constraint Logic Programming" 10:45-11:15 Nataliia Stulova, Jose F. Morales and Manuel V. Hermenegildo "Assertion-based Debugging of Higher-Order (C)LP Programs" Break - 11:15-11:30 Session - 11:30-12:30 11:30:-12:00 Takahito Aoto and Sorin Stratulat "Decision Procedures for Proving Inductive Theorems without Induction" 12:00-12:30 Joachim Jansen, Ingmar Dasseville, Jo Devriendt and Gerda Janssens "Experimental Evaluation of a State-of-the-Art Grounder" Lunch break - 12:30-13:30 Session - 13:30-14:30 13:30:-14:00 Tom Schrijvers, Nicolas Wu, Benoit Desouter and Bart Demoen "Heuristics entwined with handlers combined" 14:00-14:30 James Cheney, Amal Ahmed and Umut Acar "Database queries that explain their work" ========== Also, please note a change of dates: LOPSTR will start on September 9, rather than September 10 as previously announced. See you in Canterbury!

1 0

ANNOUNCE: hplayground: haskell client-side web framework
by Alberto G. Corona 26 Jul '14

26 Jul '14

hplayground [1] is a haskell framework that compiles to JavaScript with the haste [5] compiler. It handles reactive effects under a applicative-monad that controls the modifications of the user interface. It is quite easy to create dynamic, composable applications using ordinary, beatiful, idiomatic haskell without special constructions. Rather than a framework, it is an EDSL. Full reinversion of control avoid spagetty event handlers and the monad confines the events and their effects to the subtree where they appear avoiding the problems of declarative reactive frameworks. There are examples running[4] the source code is in [1] And there is a todo reference application [3] running [2] too. There is also a blog post about that[7] Additionally, the syntax is almost identical to the formlet widgets in MFlow[6]. So most of the hplaygroud code could run also in a server if javascript is disabled. But MFlow and hplayground are completely independent projects. I hope that you enjoy it as much as I enjoyed the development of it. A big thanks to Anton Ekblad for his wonderful Haste compiler. [1] https://github.com/agocorona/hplayground [2] http://mflowdemo.herokuapp.com/todo.html [3] https://github.com/agocorona/hplay-todo [4] http://mflowdemo.herokuapp.com/noscript/wiki/browserwidgets [5] http://http://haste-lang.org/ [6] http://hackage.haskell.org/package/MFlow [7] http://haskell-web.blogspot.com.es/2014/07/hplayground-translate-your-conso… -- Alberto.

1 0

HOPE 2014 Call for Participation (with Workshop Program)
by Hongseok Yang 24 Jul '14

24 Jul '14

---------------------------------------------------------------------- CALL FOR PARTICIPATION HOPE 2014 The 3rd ACM SIGPLAN Workshop on Higher-Order Programming with Effects August 31, 2014 Gothenburg, Sweden (the day before ICFP 2014) https://www.mpi-sws.org/~neelk/hope2014/ ---------------------------------------------------------------------- HOPE 2014 aims at bringing 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. ------------ Registration ------------ Deadline for early registration: 3 August 2014 Web site: https://regmaster4.com/2014conf/ICFP14/register.php This is the registration site for ICFP 2014 and all the affiliated workshops including HOPE 2014. ------------ Invited Talk ------------ Title: Verifying Security Properties of SES Programs Speaker: Philippa Gardner, Imperial College London ---------------------- List of Accepted Talks ---------------------- (1) Stevan Andjelkovic. Towards indexed algebraic effects and handlers (2) Kwok Cheung. Separating Entangled State (3) Filip Sieczkowski and Lars Birkedal. ModuRes: a Coq Library for Reasoning about Concurrent Higher-Order Imperative Programming Languages (4) Ohad Kammar. Graphical algebraic foundations for monad stacks (5) Paul Downen and Zena M. Ariola. Delimited control with multiple prompts in theory and practice (6) Carter Schonwald. A Type Directed model of Memory Locality and the design of High Performance Array APIs (7) Georg Neis, Chung-Kil Hur, Jan-Oliver Kaiser, Derek Dreyer and Viktor Vafeiadis. Compositional Compiler Verification via Parametric Simulation (8) Danel Ahman and Tarmo Uustalu. From stateful to stackful computation --------------------- 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. --------------------- Workshop Organization --------------------- Program Co-Chairs: Neel Krishnaswami (University of Birmingham) Hongseok Yang (University of Oxford) Program Committee: Zena Ariola (University of Oregon) Ohad Kammar (University of Cambridge) Ioannis Kassios (ETH Zurich) Naoki Kobayashi (University of Tokyo) Paul Blain Levy (University of Birmingham) Aleks Nanevski (IMDEA) Scott Owens (University of Kent) Sam Staton (Radboud University Nijmegen) Steve Zdancewic (University of Pennsylvania)

1 0