February 2014 - Haskell

Call for papers: HLPP 2014 - 7th Symposium on High-Level Parallel Programming and Applications
by Clemens Grelck 18 Feb '14

18 Feb '14

=========================================================================== CALL FOR PAPERS HLPP 2014 7th International Symposium on High-level Parallel Programming and Applications Amsterdam, Netherlands July 3-4, 2014 https://sites.google.com/site/hlpp2014amsterdam/ =========================================================================== Aims and scope: As processor and system manufacturers increase the amount of both inter- and intra-chip parallelism it becomes crucial to provide the software industry with high-level, clean and efficient tools for parallel programming. Parallel and distributed programming methodologies are currently dominated by low-level techniques such as send/receive message passing, or equivalently unstructured shared memory mechanisms. Higher-level, structured approaches offer many possible advantages and have a key role to play in the scalable exploitation of ubiquitous parallelism. Since 2001 the HLPP series of workshops/symposia has been a forum for researchers developing state-of-the-art concepts, tools and applications for high-level parallel programming. The general emphasis is on software quality, programming productivity and high-level performance models. The 7th Symposium on High-Level Parallel Programming and Applications will be held July 3-4 in the historic center of Amsterdam. =========================================================================== Proceedings: Accepted papers will be distributed as informal draft proceedings during the symposium. All accepted papers will be published by Springer in a special issue of the International Journal of Parallel Programming (IJPP). =========================================================================== Important dates: Submission deadline: April 4 (anywhere on earth) Author notification: May 1 Camera-ready paper due: June 16 =========================================================================== Topics: HLPP 2014 invites papers on all topics in high-level parallel programming, its tools and applications including, but not limited to, the following aspects: + High-level programming and performance models (BSP, CGM, LogP, MPM, etc.) and their tools + Declarative parallel programming methodologies + Algorithmic skeletons and constructive methods + Declarative parallel programming languages and libraries: semantics and implementation + Verification of declarative parallel and distributed programs + Software synthesis, automatic code generation for parallel programming + Model-driven software engineering with parallel programs + High-level programming models for heterogeneous/hierarchical platforms + High-level parallel methods for large datasets + Applications of parallel systems using high-level languages and tools + Teaching experience with high-level tools and methods =========================================================================== Paper preparation and submission: Papers submitted to HLPP2014 must describe original research results and must not have been published or simultaneously submitted anywhere else. Manuscripts must be prepared with the Springer IJSS latex macro package and submitted via the EasyChair Conference Management System. Each paper will receive a minimum of three reviews by members of the international technical programme committee (see below). Papers will be selected based on their originality, relevance, technical clarity and quality of presentation. At least one author of each accepted paper must register for the HLPP 2014 symposium and present the paper. =========================================================================== HLPP Organizer and programme chair: Clemens Grelck Informatics Institute University of Amsterdam Science Park 904 1098XH Amsterdam Netherlands c.grelck(a)uva.nl =========================================================================== HLPP steering committee: Clemens Grelck (Universiteit van Amsterdam, Netherlands) Gaétan Hains (Université Paris-Est, France) Kiminori Matsuzaki (Kochi University of Technology, Japan) Frédéric Loulergue (Université d'Orléans, France) Quentin Miller (Somerville College Oxford, United Kingdom) Alexander Tiskin (University of Warwick, United Kingdom) =========================================================================== Previous HLPP symposia and workshops: HLPP 2013, Paris, France HLPP 2011, Tokyo, Japan HLPP 2010, Baltimore, USA HLPP 2005, Coventry, United Kingdom HLPP 2003, Paris, France HLPP 2001, Orléans, France =========================================================================== -- ---------------------------------------------------------------------- Dr Clemens Grelck Science Park 904 University Lecturer 1098XH Amsterdam Netherlands University of Amsterdam Institute for Informatics T +31 (0) 20 525 8683 Computer Systems Architecture Group F +31 (0) 20 525 7490 Office C3.105 www.science.uva.nl/~grelck ----------------------------------------------------------------------

1 0

Call for papers: HLPP 2014 - 7th Symposium on High-Level Parallel Programming and Applications
by Clemens Grelck 18 Feb '14

18 Feb '14

=========================================================================== CALL FOR PAPERS HLPP 2014 7th International Symposium on High-level Parallel Programming and Applications Amsterdam, Netherlands July 3-4, 2014 https://sites.google.com/site/hlpp2014amsterdam/ =========================================================================== Aims and scope: As processor and system manufacturers increase the amount of both inter- and intra-chip parallelism it becomes crucial to provide the software industry with high-level, clean and efficient tools for parallel programming. Parallel and distributed programming methodologies are currently dominated by low-level techniques such as send/receive message passing, or equivalently unstructured shared memory mechanisms. Higher-level, structured approaches offer many possible advantages and have a key role to play in the scalable exploitation of ubiquitous parallelism. Since 2001 the HLPP series of workshops/symposia has been a forum for researchers developing state-of-the-art concepts, tools and applications for high-level parallel programming. The general emphasis is on software quality, programming productivity and high-level performance models. The 7th Symposium on High-Level Parallel Programming and Applications will be held July 3-4 in the historic center of Amsterdam. =========================================================================== Proceedings: Accepted papers will be distributed as informal draft proceedings during the symposium. All accepted papers will be published by Springer in a special issue of the International Journal of Parallel Programming (IJPP). =========================================================================== Important dates: Submission deadline: April 4 (anywhere on earth) Author notification: May 1 Camera-ready paper due: June 16 =========================================================================== Topics: HLPP 2014 invites papers on all topics in high-level parallel programming, its tools and applications including, but not limited to, the following aspects: + High-level programming and performance models (BSP, CGM, LogP, MPM, etc.) and their tools + Declarative parallel programming methodologies + Algorithmic skeletons and constructive methods + Declarative parallel programming languages and libraries: semantics and implementation + Verification of declarative parallel and distributed programs + Software synthesis, automatic code generation for parallel programming + Model-driven software engineering with parallel programs + High-level programming models for heterogeneous/hierarchical platforms + High-level parallel methods for large datasets + Applications of parallel systems using high-level languages and tools + Teaching experience with high-level tools and methods =========================================================================== Paper preparation and submission: Papers submitted to HLPP2014 must describe original research results and must not have been published or simultaneously submitted anywhere else. Manuscripts must be prepared with the Springer IJSS latex macro package and submitted via the EasyChair Conference Management System. Each paper will receive a minimum of three reviews by members of the international technical programme committee (see below). Papers will be selected based on their originality, relevance, technical clarity and quality of presentation. At least one author of each accepted paper must register for the HLPP 2014 symposium and present the paper. =========================================================================== HLPP Organizer and programme chair: Clemens Grelck Informatics Institute University of Amsterdam Science Park 904 1098XH Amsterdam Netherlands c.grelck(a)uva.nl =========================================================================== HLPP steering committee: Clemens Grelck (Universiteit van Amsterdam, Netherlands) Gaétan Hains (Université Paris-Est, France) Kiminori Matsuzaki (Kochi University of Technology, Japan) Frédéric Loulergue (Université d'Orléans, France) Quentin Miller (Somerville College Oxford, United Kingdom) Alexander Tiskin (University of Warwick, United Kingdom) =========================================================================== Previous HLPP symposia and workshops: HLPP 2013, Paris, France HLPP 2011, Tokyo, Japan HLPP 2010, Baltimore, USA HLPP 2005, Coventry, United Kingdom HLPP 2003, Paris, France HLPP 2001, Orléans, France =========================================================================== -- ---------------------------------------------------------------------- Dr Clemens Grelck Science Park 904 University Lecturer 1098XH Amsterdam Netherlands University of Amsterdam Institute for Informatics T +31 (0) 20 525 8683 Computer Systems Architecture Group F +31 (0) 20 525 7490 Office C3.105 www.science.uva.nl/~grelck ----------------------------------------------------------------------

1 0

5 PhD Positions in Formal Methods, Functional Programming, and Information and Software/Web Security at the Chalmers University of Technology, Sweden
by Laura Kovacs 17 Feb '14

17 Feb '14

5 PhD Positions in Formal Methods, Functional Programming, and Information and Software/Web Security at the Department of Computer Science and Engineering, Chalmers University of Technology, Sweden Application deadline: March 31, 2014 Expected starting date of positions: September 1, 2014 ------------------------------------------------------------------------ *Job description* The Department of Computer Science and Engineering at Chalmers University of Technology invites applications for PhD positions in Formal Methods/Automated Reasoning, Functional Programming, and Information and Software/Web Security, as follows: ----------------------------- * 1 PhD position in Formal Methods: The PhD student will join the Formal Methods group and contribute to its research on improving the quality of complex software systems. The Formal Methods group of Chalmers is an internationally recognised research group with a high-profile research track record and an excellent network of collaborators. The group's research focus is in the theoretical and practical aspects of formal software verification, including automated reasoning, interactive theorem proving, runtime verification, and test generation. Together with international collaborators, the group members co-developed widely recognised verification tools like KeY ( www.key-project.org) Vampire (http://vprover.org) ALIGATOR ( mtc.epfl.ch/software-tools/Aligator), and LARVA. The research of the advertised PhD position will be in the area of Software Verification, with a strong focus on the creative use and development of automated reasoning techniques for software verification. In particular, we are interested in designing and combining new methods in automated first-order theorem proving, satisfiability modulo theory solvers, symbolic computation, and program analysis for the generation and verification of complex program properties, such as invariants, interpolants, pre- and post-conditions. Background in one or more of the following areas is expected: logic, formal methods, formal verification. This position will be supervised by Prof. Laura Kovacs in the frame of her recently granted junior researcher project by the Swedish Research Council. Laura Kovacs is the main developer of the ALIGATOR tool and the co-developer of the world-leading theorem prover Vampire for applications of program analysis and verification. ----------------------------- * 1 PhD Position in Functional Programming The PhD student will join the Chalmers Functional Programming (FP) Group, one of the leading groups in the field. The Chalmers FP Group has a strong interest in Embedded Domain Specific Languages, beginning with their work on Lava for hardware design. The focus of the advertised position is on returning to the problem of how to use Functional Programming to support hardware design and deterministic parallel programming. We are particularly interested in the implementation of cryptographic algorithms. Our favoured platform is the open source Parallella board from Adapteva (http://www.adapteva.com/parallella-board/) which combines Field Programmable Gate Array (FPGA), two ARM cores and 16 or 64 cores connected in a grid. This small board promises high performance, low power computing, but the question of how best to program it is an interesting one. The new PhD student will work on the use of Functional Programming to enable programming of such highly parallel heterogeneous systems. The ideal candidate for the position in Functional Programming will have a strong background in functional programming and at least one of hardware design and parallel programming. The PhD student will be supervised by Prof. Mary Sheeran, who has long pioneered the combination of hardware design and functional programming, particularly working with her former students Koen Claessen and Satnam Singh. The work will be closely connected to the SSF funded project on Productivity and Performance through Resource Aware Functional Programming ( http://www.cse.chalmers.se/~ms/SSF10Final.pdf) ----------------------------- * 1 PhD Position in Information Security The PhD student will join the Chalmers Information Security group, working in the area of information and communication security with a focus on authentication problems in constrained settings. This is particularly important for applications involving mobile phones, wireless communication and RFID systems, which suffer from restrictions in terms of power resources, network connectivity, computational capabilities, as well as potential privacy issues. The overall aim of the announced PhD position will be to develop nearly optimal algorithms for achieving security and privacy while minimising resource use. More concretely, part of the research will involve the analysis and development of authentication protocols in specific settings. This will include investigating resistance of both existing and novel protocols against different types of attacks, theoretically and experimentally. In addition to investigating established settings, such as RFID authentication, the research will also explore more general authentication problems, such as those that arise in the context of trust in social networks, smartphone applications and collaborative data processing. This will be done by grounding the work in a generalised decision-making framework. The project should result in the development of theory and authentication mechanisms for noisy, constrained settings that strike an optimal balance between reliable authentication, privacy-preservation and resource consumption. Experience in one or more of cryptography, probability and statistics, decision and game theory are beneficial. Mathematical maturity is essential. The PhD student will be supervised by Prof. Katerina Mitrokotsa and will have the chance to collaborate with well-known researchers in the area of information security. Some previous research related to this research project can be found here: http://www.cse.chalmers.se/~aikmitr/ . Katerina Mitrokotsa's research is currently funded by the European Commission and the Chalmers ICT Areas of advance. --------------------------------- * 2 PhD Positions in Software/Web Security The PhD students will join a world-leading team of researchers on software security. Software is often the root cause of vulnerabilities in modern computing systems such as the web. By focusing on securing the software, we target principled security mechanisms that provide robust protection against large classes of attacks. The focus of the advertised positions is on the following directions of work: - To design rich security policies for confidentiality, integrity and availability, as demanded by practical applications (such as web and mobile applications). - To develop practical enforcement mechanisms for these policies in expressive programming languages (such as web and mobile languages). These enforcement mechanisms may combine static (for example, static program analysis-based) and dynamic (for example, run-time execution monitoring-based) techniques. - To support the above with case studies in web-application security. In pursuing these goals, there are possibilities for collaboration with our high-profile academic and industrial partners. We run a number of ambitious projects with top international partners in academia and industry, including the European project WebSand on web application security: https://www.websand.eu/ These positions will be supervised by Prof. Andrei Sabelfeld, recipient of a number of recent awards, including SSF Advancement of Research Leaders award (2008), Chalmers Research Supervisor of the Year (2010), and ERC Starter/Consolidator (2012). Promotional video about the team's research on securing web applications: http://vimeo.com/82206652 ------------------------------------------------------------------------ *Details about Employment* PhD student positions are limited to five years and normally include 20 per cent departmental work, mostly teaching duties. Salary for the position is as specified in Chalmers' general agreement for PhD student positions. Currently the starting salary is 26,250SEK a month before tax. The positions are intended to start in fall 2014. ------------------------------------------------------------------------ *Suitable Background* Applicants should have a Master's Degree or corresponding degree in Computer Science, Computer Engineering, or in a related discipline. As for all PhD studies, a genuine interest and curiosity in the subject matter and excellent analytical and communication skills, both oral and written, are needed. You may apply even if you have not completed your degree, but expect to do so before the position starts. Knowledge of Swedish is not a prerequisite for applying since English is our working language for research, and we publish internationally. Both Swedish and English are used in undergraduate courses. Half of our researchers and PhD students at the department come from more than 30 different countries. ------------------------------------------------------------------------ *How to apply* The application should be written in English and include the following items: 1. An application of a maximum of one A4 page summarising your track record and providing your research statement 2. Attested copies of education certificates, including grade reports and other documents 3. Curriculum Vitae 4. Letters of recommendation and name of reference persons 5. Evidence of written work: research papers and theses It is important to include parts of your own work such as theses and articles that you have authored or co-authored. Please notice also that it is highly recommended that you include letters of recommendation; we typically get a large number of applications, and it is not feasible for us to request individual letters. The application should be submitted electronically by March 31, 2014, at: - for the position in Formal Methods: http://www.chalmers.se/en/about-chalmers/vacancies/?rmpage=job&rmjob=1911 - for the position in Functional Programming: http://www.chalmers.se/en/about-chalmers/vacancies/?rmpage=job&rmjob=1912 - for the position in Information Security: http://www.chalmers.se/en/about-chalmers/vacancies/Pages/default.aspx?rmpag… - for the positions in Software/Web Security: http://www.chalmers.se/en/about-chalmers/vacancies/?rmpage=job&rmjob=1913 The selection of the specific research topic will take into account both the interests of the new PhD student and the research agenda of the respective group. ------------------------------------------------------------------------ *Contact persons for further information:* Laura Kovacs <laura.kovacs(a)chalmers.se>, Formal Methods: http://www.cse.chalmers.se/~laurako/ Katerina Mitrokotsa <aikaterini.mitrokotsa(a)chalmers.se>, Information Security: http://www.cse.chalmers.se/~aikmitr/ Andrei Sabelfeld <andrei(a)chalmers.se>, Software/Web Security: http://www.cse.chalmers.se/~andrei/ Mary Sheeran <mary.sheeran(a)chalmers.se>, Functional Programming: http://www.cse.chalmers.se/~ms/ ------------------------------------------------------------------------ *The Department* The Department has about 70 faculty members and enrols about 90 PhD students from more than 30 countries. The research spans the whole spectrum, from theoretical foundations to applied systems development. There is extensive national and international collaboration with academia and industry all around the world. For more information, see http://www.chalmers.se/cse/EN/ . ------------------------------------------------------------------------ *Gothenburg, Sweden* Gothenburg is often referred to as the "heart of Scandinavia". The videos below give an impression what it's like to live and study in Gothenburg. Live in Gothenburg: http://youtu.be/sbwVIQeGcdY Study in Gothenburg: http://youtu.be/0WrlGlSyS1c ------------------------------------------------------------------------

1 0

ANN: Simon Marlow & Edward Kmett @ ZuriHac 2014
by Bas van Dijk 14 Feb '14

14 Feb '14

Dear Haskellers and ZuriHac 2014 attendees, On this lovely day (pun intended), I'm excited to announce that Simon Marlow and Edward Kmett will be giving talks at ZuriHac 2014. When: Friday 6 June 2014 - Sunday 8 June 2014 Where: Erudify offices, Zurich, Switzerland ZuriHac is an international Haskell hackathon: a grassroots, collaborative coding festival with a simple focus, to build and improve Haskell libraries, tools, and infrastructure. This is a great opportunity to meet your fellow Haskellers in real life, find new contributors for your project, improve existing libraries and tools, or even start new ones! 30 people already signed up for ZuriHac 2014 but there's still room for more. If you wish to attend, please register by filling in this form: http://bit.ly/ZuriHac2014 Full details can be found on the wiki page: http://www.haskell.org/haskellwiki/ZuriHac2014 We look forward to seeing you there! -- The organisers of ZuriHac 2014 ZuriHac 2014 is sponsored by Erudify & Google

1 0

Fun in the Afternoon @Facebook, March 12 2014: Schedule
by Simon Marlow 13 Feb '14

13 Feb '14

I had an incredible response to the call for talks for Fun @Facebook, thanks to everyone who offered a talk! The schedule and abstracts are below. As you can see, I've kept the slots short (25 minutes) in order to fit in 9 talks and 2 breaks. Time will be tight, but it should be good Fun. More details about logistics to follow. Schedule: March 12 ================== 12.00-1.00 grab some lunch nearby, then head to Facebook London ------------ 1.00 José Pedro Magalhães: Chordify: Advanced Functional Programming for Fun and Profit 1.25 Dominic Orchard: Fun with indexed monads 1.50 Patrick Chilton and Niklas Hambuchen: Brain reading with Hemokit 2.15-2.45 BREAK ------------ 2.45 Claudio Russo: Tabular: A DSL for Probabilistic Inference from Excel 3.10 Duncan Coutts: Binary serialisation: better, stronger, faster 3.35 Ben Ford: Haskell in production 4.00-4.30 BREAK ------------ 4.30 Tarmo Uustalu: Update monads, or how you always wanted to combine reading and writing 4.55 Dominic Steinitz: Automatic Differentiation: A Criminally Underused Tool? 5.20 Maceij Pirog: FizzBuzz in Haskell by Embedding a Domain-Specific Language 5.45 END (pub + food) Abstracts ========= José Pedro Magalhães Chordify: Advanced Functional Programming for Fun and Profit Abstract Functional programming, especially when using advanced techniques such as GADTs, type functions, and kind polymorphism, is not only fun; it can also be profitable. In this talk I'll describe my experience in using advanced functional programming in Haskell within Chordify, a web startup that brings chord recognition to the masses. ------------- Dominic Orchard Fun with indexed monads Monads are well established as an abstraction technique for programming with effects of various kinds. At the type-level, monads present a black-box view of effects: for some notion of effect, a computation is either effectful or not. This contrasts with the richer information provided by effect systems. Various work has unified monads and effect systems, both syntactically (Wadler & Thiemann, 2003) and semantically (Katsumata, 2014). In this talk, I show how to program with "indexed monads" in Haskell which semantically unify monads and effects, where a monadic type constructor is indexed by a monoid of effect information. A number of examples are shown, including verifying finite-element computations in scientific computing using indexed monads. This is joint work with Tomas Petricek, Andrew Rice, and Alan Mycroft. ------------- Patrick Chilton and Niklas Hambuchen Brain reading with Hemokit We present our Haskell driver for the Emotiv EEG and how you can use it to control your computer with your brain. We might discuss good and bad experiences in binding-writing and might try to abuse the audience to solve our problems. ------------- Claudio Russo Tabular: A DSL for Probabilistic Inference from Excel Joint work with: Andy Gordon, Thore Graepel, Nicolas Rolland, Johannes Borgström, John Guiver, Marcin Szymczak Tabular is a probabilistic functional language embedded in Excel. Tabular brings the power of machine learning to data enthusiasts - the large class of end users who wish to model and learn from their data, who have some knowledge of probability distributions and data schemas, but who are not necessarily professional developers. Tabular is an Excel plugin that provides a much simpler, interactive interface to the underlying Infer.NET inference engine. Tabular helps the data enthusiast model and visualize their data. Tabular automatically suggests a model from the data schema, allows the enthusiast to edit and refine the model, infers model parameters from data and predicts missing values, and visualizes the results using Excel's standard features. The ability to query for missing values provides a uniform interface to a wide variety of tasks, including classification, clustering, recommendation, and ranking. Tabular is based on probabilistic programming technology, which enables a wide range of machine learning algorithms to be constructed based on a probabilistic model. A unique feature is that Tabular models are simply succinct annotations on the relational schema of the Excel data model. The talk will give an overview and demo of the language in action. ------------- Duncan Coutts Binary serialisation: better, stronger, faster This talk is about a new implementation of binary serialisation for Haskell's 'binary' package. It is faster -- much faster -- and produces smaller binary output, but just as importantly it provides a story for versioning and migration and the ability to view the binary data without a schema. We will look at the binary format of the current binary (and cereal) packages and see why it makes developers nervous and excludes potential uses. We will describe some of the qualities that we want from a serialisation format, the particular format choice that we have settled on and how we can implement versioning/migration. We will also look at the performance side of things: why the existing binary serialisation packages are not as fast as they could be and at the key tricks -- high level and low level -- in the new implementation. There will be quite a bit of GHC-core code diving and discussion of evaluation and runtime issues. Some of these optimisation tricks or analysis techniques may be useful in your own projects, and should give you a renewed appreciation for GHC's capabilities. ------------- Ben Ford Haskell in Production Fynder is a start up building a platform for discovering and booking services across multiple different industries. This talk will be about how we tackle the problem and how we've built a development, testing and deployment environment around Haskell as the core language. ------------- Tarmo Uustalu Update monads, or how you always wanted to combine reading and writing Did it ever trouble you that, despite feeling a bit like it, state monads fail to be a common generalization of reader and writer monads? I will introduce you to update monads, a true generalization of reader and writer monads that is moreover as canonical as it gets. An update monad is given by a set (of states), a monoid (of updates) and an action of the monoid on the set (defining the effect of every update on every state). Update monads are exactly the compatible compositions of reader and writer monads, which are in a bijection with distributive laws between reader and writer monads. State monads are canonically related to those update monads where the monoid of updates is the free monoid on the overwrite semigroup structure on the set of states. Update monads do not just have a clean theoretical motivation; embracing many natural examples, they are also a practical abstraction. A finer dependently-typed variation of the concept has every state coming with its own set of enabled updates. This is joint work with Danel Ahman, University of Edinburgh. ------------- Dominic Steinitz Automatic Differentiation: A Criminally Underused Tool? Artificial Neural Networks (ANNs) are a well-established Machine Learning (ML) technique. Traditionally, training ANNs is done using a technique called backpropogation. It turns out that this is just a specialised version of Reverse Automatic Differentiation (RAD) and steepest descent. This talk explains the theory behind RAD and develops an implementation in Haskell of Forward Automatic Differentiation (FAD) with a brief application to another ML technique: regression. ------------- Maceij Pirog FizzBuzz in Haskell by Embedding a Domain-Specific Language The FizzBuzz problem is simple but not trivial, which makes it a popular puzzle during job interviews for software developers. The conundrum lies in a peculiar but not unusual control-flow scenario: the default action is executed only if some previous actions were not executed. In this tutorial we ask if we can accomplish this without having to check the conditions for the previous actions twice; in other words, if we can make the control flow follow the information flow without loosing modularity. And the contest is for beauty of the code. We deliver a rather non-standard, and a bit tongue-in-cheek solution. First, we design a drastically simple domain-specific language (DSL), which we call, after the three commands of the language, Skip-Halt-Print. For each natural number n, we devise a Skip-Halt-Print program that solves FizzBuzz for n. Then, we implement this in Haskell, and through a couple of simple transformations we obtain the final program. The corollary is a reminder of the importance of higher-order functions in every functional programmer s toolbox.

1 0

CFP: Term and Graph rewriting, special issue of MSCS
by Rachid Echahed 13 Feb '14

13 Feb '14

-------------------------------------------------------------------------- First Call for Papers Special Issue of Mathematical Structures in Computer Science (MSCS) on "TERM and GRAPH Rewriting" -------------------------------------------------------------------------- Scope -------------------------------------------------------------------------- Rewriting techniques constitute a foundational theory of computing science. They are being investigated for several structures such as lambda-terms, first-order terms or graphs and have been successfully used in many areas such as programming languages, automated reasoning, program verification, security, etc. This is witnessed by the leading international events ICGT, RTA or TLCA among others. During the last decade, a particular interest has been devoted to the study of the impact of shared structures in term and graph rewriting through the international editions of TERMGRAPH series of workshops. Sharing is indeed ubiquitous in several research areas, for instance: the modelling of first- and higher-order term rewriting by (acyclic or cyclic) graph rewriting, the modelling of biological or chemical abstract machines, the implementation techniques of programming languages. Term and graph rewriting are also used in automated theorem proving and symbolic computation systems working on shared structures... This special issue is devoted to recent developments in all aspects of TERM and GRAPH rewriting. This includes (but is not limited to): term rewriting, graph transformation, proof methods, programming languages, infinitary rewriting, rewrite strategies, semantics, properties of rewriting ... -------------------------------------------------------------------------- Submissions -------------------------------------------------------------------------- Submitted papers must be original and not submitted for publication elsewhere, and will be subject to the standard journal refereeing process of the Mathematical Structures in Computer Science (MSCS) journal. Submissions should be in pdf format following the MSCS instruction for contributors (http://assets.cambridge.org/MSC/MSC_ifc.pdf) and should be submitted electronically via the following easy-chair web site: https://www.easychair.org/conferences/?conf=mscsrewriting2012 -------------------------------------------------------------------------- Important Dates -------------------------------------------------------------------------- January 20, 2012 : Abstract submission February 20, 2012: Paper submission June 15, 2012 : Notification of acceptance -------------------------------------------------------------------------- Guest Editor: -------------------------------------------------------------------------- Rachid Echahed, CNRS LIG Lab., Grenoble, France echahed(a)imag.fr --------------------------------------------------------------------------

1 8

RV 2014: 2nd Call for Papers, Deadline in 2 months
by Runtime Verification 12 Feb '14

12 Feb '14

[Apologizes for duplicates] 14th International Conference on Runtime Verification September 22 - 25, 2014 *Toronto, Canada* http://rv2014.imag.fr/ <http://rv2014.imag.fr/images/CfP.pdf> Scope: Runtime verification is concerned with monitoring and analysis of software and hardware system executions. Runtime verification techniques are crucial for system correctness, reliability, and robustness; they are significantly more powerful and versatile than 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. Technical Research Papers Track: Technical research papers can be submitted in two categories: regular and short papers. Papers in both categories will be reviewed by the conference Program Committee. All accepted technical papers will appear in an LNCS<http://www.springer.com/series/558> volume. Submitted papers must use the LNCS style<http://www.springer.com/computer/lncs?SGWID=0-164-6-793341-0>. At least one author of each accepted paper must attend RV'14 to present the paper. Papers must be submitted electronically using theEasyChair<https://www.easychair.org/conferences/?conf=rv2014> system. - *Regular papers* (up to 15 pages) should present original unpublished results. Theoretical and experimental papers as well as papers on applications of runtime verification and case studies are all welcome. A non-monetary Best Paper Award will be given. A selection of accepted regular papers will be invited to appear in a special issue of the Springer Journal on Formal Methods in System Design. - *Short papers* (up to 5 pages) may present novel but not necessarily thoroughly worked out ideas, for example emerging runtime verification techniques and applications, or techniques and applications that establish relationships between runtime verification and other domains. Accepted short papers will be presented in special short talk (10 minutes) and poster sessions. Program committee Borzoo Bonakdarpour <https://cs.uwaterloo.ca/~bbonakda/> (University of Waterloo, Canada), *co-chair* Scott Smolka <http://www.cs.sunysb.edu/~sas/> (Stony Brook Universtiy, USA), *co-chair* Gul Agha <http://cs.illinois.edu/directory/profile/agha> (University of Illinois at Urbana-Champaign, USA) Thomas Ball <http://research.microsoft.com/en-us/people/tball/> (Microsoft Research, Redmond, USA) Howard Barringer <http://www.manchester.ac.uk/research/howard.barringer> (The University of Manchester, UK) Ezio Bartocci <http://www.eziobartocci.com/> (TU Wien, Austria) David Basin <http://www.inf.ethz.ch/personal/basin/> (ETH Zurich, Switzerland) Saddek Bensalem <http://www-verimag.imag.fr/~bensalem/> (Verimag, France) Eric Bodden <http://www.bodden.de/> (TU - Darmstadt, Germany) Ivona Brandic <http://www.infosys.tuwien.ac.at/staff/ivona/> (TU Wien, Austria) Marsha Chechik <http://www.cs.toronto.edu/~chechik/> (University of Toronto, Canada) Michael Clarkson <http://faculty.cs.gwu.edu/~clarkson/> (George Washington University, USA) Laura Dillon <http://www.cse.msu.edu/~ldillon/> (Michigan State University, USA) Shlomi Dolev <http://www.cs.bgu.ac.il/~dolev/> (Ben Gurion University, Israel) Alastair Donaldson <http://www.doc.ic.ac.uk/~afd/> (Imperial College London, UK) Dawson Engler <http://www.stanford.edu/~engler/> (Stanford University, USA) Ylies Falcone <http://www.ylies.fr/> (Université Joseph Fourier, France) Vijay Garg <http://users.ece.utexas.edu/~garg/> (University of Texas at Austin, USA) Steve Goddard <http://cse.unl.edu/~goddard/papers.html> (University of Nebraska-Lincoln, USA) Ganesh Gopalakrishnan <http://www.cs.utah.edu/~ganesh/> (University of Utah, USA) Wolfgang Grieskamp (Google, USA) Radu Grosu <http://www.cs.sunysb.edu/~grosu/> (TU- Wien, Austria) Klaus Havelund <http://www.havelund.com/> (NASA/JPL, USA) Mats Heimdahl <http://www.umsec.umn.edu/about/director> (University of Minnesota, USA) Laurie Hendren <http://www.sable.mcgill.ca/~hendren/> (McGill University, Canada) Gerard Holzmann <http://lars-lab.jpl.nasa.gov/people/gh.html> (NASA/JPL, USA) Daniel Keren <http://www.cs.haifa.ac.il/~dkeren/> (Haifa University, Israel) Sandeep Kulkarni <http://www.cse.msu.edu/~sandeep/>(Michigan State University, USA) Marta Kwiatkowska <http://www.cs.ox.ac.uk/marta.kwiatkowska/> (University of Oxford, UK) Insup Lee <http://www.cis.upenn.edu/~lee/home/home/index.shtml> (University of Pennsylvania, USA) Axel Legay <http://people.irisa.fr/Axel.Legay/> (IRISA/INRIA, France) Martin Leucker <http://www.isp.uni-luebeck.de/leucker/> (University of Lübeck, Germany) Leonardo Mariani<http://www.lta.disco.unimib.it/lta/personalPages/leonardoMariani/leonardoMa…> (University of Milano Bicocca, Italy) Patrick Meredith <http://fsl.cs.illinois.edu/index.php/Patrick_Meredith> (University of Illinois at Urbana-Champaign, USA) David Naumann <http://www.cs.stevens.edu/~naumann/> (Stevens Institute of Technology, USA) Doron Peled <http://u.cs.biu.ac.il/~doronp/> (Bar Ilan University, Israel) Mauro Pezze <http://www.inf.usi.ch/personal-info?id=1187> (University of Lugano, Switzerland) Lee Pike <http://www.cs.indiana.edu/~lepike/> (Galois Inc., USA) Zvonimir Rakamaric <http://www.zvonimir.info/> (University of Utah, USA) Grigore Rosu <http://fsl.cs.illinois.edu/index.php/Grigore_Rosu> (University of Illinois at Urbana-Champaign, USA) Andrey Rybalchenko <http://www7.in.tum.de/~rybal/> (TU-Munich, Germany) Andre Schiper <http://people.epfl.ch/andre.schiper?lang=fr> (EPFL, Switzerland) Oleg Sokolsky <http://www.cis.upenn.edu/~sokolsky/> (University of Pennsylvania, USA) Scott Stoller <http://www.cs.sunysb.edu/~stoller/> (Stony Brook University, USA) Serdar Tasiran <http://home.ku.edu.tr/~stasiran/> (Koc University, Turkey) Michael Whalen <http://www.umsec.umn.edu/directory/Michael-Whalen> (University of Minnesota, USA) Lenore Zuck <http://www.cs.uic.edu/~lenore/> (University of Illinois at Chicago, USA) Tool Demonstrations Track: The aim of the RV 2014 tool demonstration track is to provide an opportunity for researchers and practitioners to show and to discuss the latest advances, experiences and challenges in devising and developing reliable software tools for runtime verification. Tool demonstration papers will be reviewed by the Tools Track Program Committee. All accepted tool demonstration papers will appear in the conference proceedings LNCS volume. Submitted papers must use the LNCS style. At least one author of each accepted paper must attend RV'14 to present the paper. Papers must be submitted electronically using the EasyChair<https://www.easychair.org/conferences/?conf=rv2014> system. Tool papers should meet the following criteria: - A tool paper should present a new tool, a new tool component or novel extensions to existing tools supporting runtime verification. Each submission should be original and not published previously in a tool paper form. - Each submission must not exceed 8 pages in the LNCS/Springer proceeding format, including all text, references and figures. The paper must be written in English and provided in PDF format. - Each submission must be accompanied at the time of the submission by a short screencast (between 5-10 minutes), with voice and overlay text commentary illustrating the demonstration of the tool (a link to it should be provided in the paper). - The paper must include information on tool availability, maturity, selected experimental results and it should provide a link to a website containing the theoretical background and user guide. Furthermore, we strongly encourage authors to make their tools and benchmarks available with their submission. - Each tool paper must include a script in an appendix (not included in the page count) describing how the demo will be conducted during the conference presentation with screenshots presenting step-by-step the tool's capabilities, highlighting the main characteristics and the usage. Evaluation Each submission will be reviewed by at least four members of the tool demonstration track program committee. The evaluation criteria will include: - the presentation quality - the availability (possibly in a open-source format) of the software. - the relevance for the Runtime Verification audience - the technical soundness of the presented tool - the originality of the underlying ideas Tool Demonstration Committee Ezio Bartocci, (TU-Vienna, Austria), *Chair* Eric Bodden (TU - Darmstadt, Germany) Alastair Donaldson (Imperial College London, UK) Dawson Engler (Stanford University, USA) Ylies Falcone (Université Joseph Fourier, France) Klaus Havelund (NASA/JPL, USA) Michael Whalen (University of Minnesota, USA) Important Dates: Both research papers and tool demonstration tracks will follow the following timeline: - *Abstract deadline:* April 8, 2014 - *Full paper deadline:* April 15, 2014 - *Rebuttal phase:* May 18-20, 2014 - *Acceptance notification:* June 10, 2014 - *Camera ready submission:* June 25, 2014 - *Conference dates:* 22-25 September, 2014 Competition on Software for Runtime Verification (CSRV-2014) A satellite event of RV'14 is the first *International Competition on Software for Runtime Verification* (CRVS'14). The main aims of CSRV-2014 competition are to: - Stimulate the development of new efficient and practical runtime verification tools and the maintenance of the already developed ones. - Produce a benchmark suite for runtime verification tools, by sharing case studies and programs that researchers and developers can use in the future to test and to validate their prototypes. - Discuss the metrics employed for comparing the tools. - Provide a comparison of the tools running with different benchmarks and evaluating using different criteria. - Enhance the visibility of presented tools among the different communities (software engineering, formal methods and automated verification, distributed computing, security, and safety-critical systems) involved in software monitoring. CRVS'14 will follow the following time line: - *Declaration of intent:* December 15, 2013 - *Deadline for submission of benchmarks:* March 1, 2014 - *Monitoring tool submission:* June 1, 2014 - *Notification:* July 1, 2014 For more information, visit http://rv2014.imag.fr/monitoring-competition or contact the event organizers: - *Ezio Bartocci* (TU-Wien, Austria), ezio.bartocci(a)tuwien.ac.at - *Borzoo Bonakdarpour* (U. Waterloo, Canada), borzoo(a)cs.uwaterloo.ca - *Ylies Falcone* (U. Joseph Fourier, France), ylies.falcone(a)ujf-grenoble.fr

1 0

Midlands Graduate School in the Foundations of Computing
by Graham Hutton 11 Feb '14

11 Feb '14

Dear all, Readers of this group might be interested in the Midlands Graduate School in the Foundations of Computing, a 5-day programme of courses in theoretical computer science that runs in Nottingham, UK from 22-26 April 2014: http://www.cs.nott.ac.uk/~txa/mgs.2014/ Courses include category theory, concurrency, denotational semantics, lambda calculus, randomised search, homotopy type theory, infinite data structures, parametricity, functional reactive programming, and dependently typed programming. Best wishes, Graham -- Prof Graham Hutton Functional Programming Lab School of Computer Science University of Nottingham, UK http://www.cs.nott.ac.uk/~gmh This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please send it back to me, and immediately delete it. Please do not use, copy or disclose the information contained in this message or in any attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. This message has been checked for viruses but the contents of an attachment may still contain software viruses which could damage your computer system, you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation.

1 0

Summer School on Cyber-Physical Systems, GRENOBLE (FRANCE) JULY 7-11, 2014
by Ylies Falcone 11 Feb '14

11 Feb '14

[~~~~~~ Please disseminate widely within your teams & contacts ~~~~~~] Dear Colleagues, PERSYVAL-Lab and NASA-JPL are organizing the second edition of the CPS Summer School. The broad objective of the CPS Summer School is to explore the manifold relationship between networked embedded systems (« the internet of things ») and humans as their creators, users, and subjects. The format of the Summer School is a five days meeting, organized around different aspects of rigorous engineering of Cyber-Physical Systems. This year, the objective of the school is to survey fundamental and applied aspects of modelling, monitoring and learning of systems as well as to identify novel opportunities and research directions in these areas through a series of lectures by international experts. Participants will also experience the relevant technologies during hands-on courses and be given a chance to present their own work. The school will provide a great opportunity to know other people working in the field, to meet distinguished scholars, and to establish contacts that may lead to research collaborations in the future. The school will concentrate on the fields of system modelling, monitoring and learning. Over the last ten years we have seen a lot of growth in these areas, building on strong theoretical foundations to apply and extend techniques to new application domains. Runtime verification is a growing field with more and more efffective applications in safety/mission-critical systems, enterprise and systems software, autonomous and reactive control systems, health management and diagnosis systems, and system security and privacy. The field of specification mining (learning specifications from system behaviour) has also seen a surge in research effort, with the establishment of a number of competitions to drive forward the development of practical tools. This research community is at an ideal stage to benefit from a school such as this, to inspire, motivate and instruct new researchers into the field. Students participating at this summer school will learn the current state of the art in modeling, monitoring, and learning. Students will be able to apply new techniques coming from various communities and backgrounds to their own domain. The CPS Summer School will be held at Grenoble University. Courses will be given in English by experts from industry and academia working in various fields of CPS. Topics: • System modeling. • Monitoring. • Learning. • Medical devices. • Sensor networks. Confirmed Speakers: • Eric Bodden (TU Darmstadt and EC SPRIDE, Germany). • Olivier Coutelou (Schneider Electric, France). • Radu Grosu (Technical Univesity Wien, Austria). • Klaus Havelund (NASA JPL, USA). • Kim G. Larsen (Aalborg University, Denmark). • Martin Leucker (University of Lübeck, Germany). • Roberto Passerone (Universita' degli Studi di Trento, Italy). • Grigore Rosu (University of Illinois at Urbana Champaign, USA). • Mohamad Sawan (Ecole Polytechnique de Montréal, Canada). • Bernhard Steffen (Technical University Dortmund, Germany). • Andreas Zeller (Saarland University, Germany). Organization Committee: • Saddek Bensalem - University of Grenoble, France. • Yliès Falcone - University of Grenoble, France. • Klaus Havelund - NASA JPL, USA. Registration fee is €250 for students, €400 for non-students, which includes lunches and coffee breaks from Monday 8th through Thursday 11th, and a party. The registration fee only partially covers the costs incurred. The remaining costs are covered by PERSYVAL-Lab. The local organization committee has arranged university accommodations for students. Please refer to the Website for more details. Application Procedure and Important Dates (please refer to the Website for the full procedure): • Deadline for Application: April 14, 2014. • Response to Applicants: April 21, 2014. • Online Registration and Fee payment: May 10, 2014. • Summer school on CPS: July 7-11, 2014. Since attendance is limited, priority will be given to Ph.D. students and companies' staff. More details can be found at: https://persyval-lab.org/en/summer-school/cps14. Applications can be submitted at: https://persyval-calls.imag.fr/en/project/10. Enquiries can be sent to cps-school.organization(a)imag.fr. Best Regards, Saddek Bensalem, Yliès Falcone, and Klaus Havelund

1 0

Higher-order, Typed, Inferred, Strict: ACM SIGPLAN ML Family Workshop
by oleg＠okmij.org 11 Feb '14

11 Feb '14

[Please notice the new submission category of informed opinions and the broad scope of the workshop. Compilation techniques, run-time systems and fancy types should be of interest to the Haskell community, too.] Higher-order, Typed, Inferred, Strict: ACM SIGPLAN ML Family Workshop Thursday September 4, 2014, Gothenburg, Sweden (immediately following ICFP and preceding OCaml Users and Developers Workshop) Call For Papers http://okmij.org/ftp/ML/ML14.html ML is a very large family of programming languages that includes Standard ML, OCaml, F#, SML#, Manticore, MetaOCaml, JoCaml, Alice ML, Dependent ML, Flow Caml, and many others. All ML languages, beside the great deal of syntax, share several fundamental traits. They are all higher-order, strict, mostly pure, and typed, with algebraic and other data types. Their type systems inherit from Hindley-Milner. The development of these languages has inspired a significant amount of computer science research and influenced a number of programming languages, including Haskell, Scala and Clojure, as well as Rust, ATS and many others. ML workshops have been held in affiliation with ICFP continuously since 2005. This workshop specifically aims to recognize the entire extended ML family and to provide the forum to present and discuss common issues, both practical (compilation techniques, implementations of concurrency and parallelism, programming for the Web) and theoretical (fancy types, module systems, metaprogramming). The scope of the workshop includes all aspects of the design, semantics, theory, application, implementation, and teaching of the members of the ML family. We also encourage presentations from related languages (such as Scala, Rust, Nemerle, ATS, etc.), to exchange experience of further developing ML ideas. The ML family workshop will be held in close coordination with the OCaml Users and Developers Workshop. Format Since 2010, the ML workshop has adopted an informal model. Presentations are selected from submitted abstracts. There are no published proceedings, so any contributions may be submitted for publication elsewhere. We hope that this format encourages the presentation of exciting (if unpolished) research and deliver a lively workshop atmosphere. Each presentation should take 20-25 minutes, except demos, which should take 10-15 minutes. The exact time will be decided based on the number of accepted submissions. The presentations will likely be recorded. Post-conference proceedings We are considering post-conference proceedings of selected papers. The Program Committee shall invite interested authors of selected presentations to expand their abstract for inclusion in the proceedings. The submissions are to be reviewed according to the standards of the publication. Coordination with the OCaml Users and Developers Workshop The OCaml workshop is seen as more practical and is dedicated in significant part to the OCaml community building and the evolution of the OCaml system. In contrast, the ML family workshop is not focused on any language in particular, is more research oriented, and deals with general issues of the ML-style programming and type systems. Yet there is an overlap, which we are keen to explore in various ways. The authors who feel their submission fits both workshops are encouraged to mention it at submission time or contact the Program Chairs. Scope We acknowledge the whole breadth of the ML family and aim to include languages that are closely related (although not by blood), such as Rust, ATS, Scala, Typed Clojure. Those languages have implemented and investigated run-time and type system choices that may be worth considering for OCaml, F# and other ML languages. We also hope that the exposure to the state of the art ML might favorably influence those related languages. Specifically, we seek research presentations on topics including but not limited to * Design: concurrency, distribution and mobility, programming for the web and embedded systems, handling semi-structured data, facilitating interactive programming, higher forms of polymorphism, generic programming, objects * Implementation: compilation techniques, interpreters, type checkers, partial evaluators, runtime systems, garbage collectors, etc. * Type systems: fancy types, inference, effects, overloading, modules, contracts, specifications and assertions, dynamic typing, error reporting, etc. * Applications: case studies, experience reports, pearls, etc. * Environments: libraries, tools, editors, debuggers, cross-language interoperability, functional data structures, etc. * Education: ML and ML-like languages in college or high-school, in general or computer science curriculum. Four kinds of submissions will be accepted: Informed Positions, Research Presentations, Experience Reports and Demos. * Informed Positions: A justified argument for or against a language feature. The argument must be substantiated, either theoretically (e.g., by a demonstration of (un)soundness, an inference algorithm, a complexity analysis), empirically or by a substantial experience. Personal experience is accepted as justification so long as it is extensive and illustrated with concrete examples. * Research Presentations: Research presentations should describe new ideas, experimental results, or significant advances in ML-related projects. We especially encourage presentations that describe work in progress, that outline a future research agenda, or that encourage lively discussion. These presentations should be structured in a way which can be, at least in part, of interest to (advanced) users. * Experience Reports: Users are invited to submit Experience Reports about their use of ML and related languages. These presentations do not need to contain original research but they should tell an interesting story to researchers or other advanced users, such as an innovative or unexpected use of advanced features or a description of the challenges they are facing or attempting to solve. * Demos: Live demonstrations or short tutorials should show new developments, interesting prototypes, or work in progress, in the form of tools, libraries, or applications built on or related to ML. (You will need to provide all the hardware and software required for your demo; the workshop organizers are only able to provide a projector.) Important dates Monday May 19 (any time zone): Abstract submission Monday June 30: Author notification Thursday September 4, 2014: ML Family Workshop Submission Submissions should be at most two pages, in PDF format, and printable on US Letter or A4 sized paper. A submission should have a synopsis (2-3 lines) and a body between 1 and 2 pages, in one- or two-column layout. The synopsis should be suitable for inclusion in the workshop program. Submissions must be uploaded to the workshop submission website before the submission deadline (Monday May 19, 2014). For any question concerning the scope of the workshop or the submission process, please contact the program chair. 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) Monterey, CA, USA Keiko Nakata Tallinn University of Technology, Estonia Didier Re'my INRIA Paris-Rocquencourt, France Zhong Shao Yale University, USA Hongwei Xi Boston University, USA

1 0