January 2015 - Haskell

ANNOUNCE: ioctl 0.0.1
by Maciej Piechotka 13 Sep '15

13 Sep '15

A package for type-safe I/O control. Currently only ioctl is supported. Currently simply a extract from my tuntap fork TODO: - Return the integer as well as structure (will break the API) - Port for Windows Network.Socket.IOCtl (as soon as I manage to setup some sane environment on this platform) - Wrapping around DeviceIoControl Example (in hsc): data NotRead = NotRead instance NotRead Int where ioctlReq _ = #const FIONREAD notRead s = ioctlsocket' s NotRead Regards

2 1

CFP: UNIF 2015
by Mateu Villaret 30 Apr '15

30 Apr '15

========================================================== Call for Papers UNIF 2015 The 29th International Workshop on Unification June 28, 2015. Warsaw, Poland http://rdp15.mimuw.edu.pl/index.php?site=unif ********* part of the Federated Conference on Rewriting, Deduction, and Programming (RDP'15) ========================================================== UNIF 2015 is the 29th event in a series of international meetings devoted to unification theory and its applications. Unification is concerned with the problem of identifying terms, finding solutions for equations, or making formulas equivalent. It is a fundamental process used in a number of fields of computer science, including automated reasoning, term rewriting, logic programming, natural language processing, program analysis, types, etc. The International Workshop on Unification (UNIF) is a yearly forum for researchers in unification theory and related fields to meet old and new colleagues, to present recent (even unfinished) work, and to discuss new ideas and trends. It is also a good opportunity for young researchers and scientists working in related areas to get an overview of the current state of the art in unification theory. Topics of Interest ------------------ A non-exhaustive list of topics of interest include: - Unification algorithms, calculi and implementations - Equational unification and unification modulo theories - Unification in modal, temporal and description logics - Admissibility of inference rules - Narrowing - Matching algorithms - Constraint solving - Combination problems - Disunification - Higher-Order unification - Type checking and reconstruction - Typed unification - Complexity issues - Query answering - Implementation techniques - Applications of unification - Antiunification/Generalization Submission ---------- Following the tradition of UNIF, we call for submissions of abstracts (5 pages) in EasyChair style, to be submitted electronically as PDF files through the EasyChair submission site: https://easychair.org/conferences/?conf=unif2015 Abstracts will be evaluated by the Programme Committee (if necessary with support from external reviewers) regarding their significance for the workshop. Accepted abstracts will be presented at the workshop and included in the informal proceedings of the workshop, available in printed form at the workshop and in electronic form from the UNIF homepage: http://www.pps.jussieu.fr/~treinen/unif/ Based on the number and quality of submissions we will decide whether to organize a special journal issue. Important Dates --------------- * Paper Submission: May 3, 2015 * Notification of Acceptance: May 31, 2015 * Final version: June 7, 2015 * Conference: June 28, 2015 Programme Committee ------------------- * Franz Baader, TU Dresden, Germany * Santiago Escobar, Universitat Politecnica de Valencia, Spain (co-chair) * Adria Gascon, SRI international, USA * Silvio Ghilardi, Universita di Milano, Italy * Artur Jez, MPI, Germany * Temur Kutsia, RISC, Johannes Kepler University Linz, Austria * Jordi Levy, IIIA-CSIC, Spain * Christopher Lynch, Clarkson University, USA * George Metcalfe, University of Bern, Switzerland * Paliath Narendran, University at Albany-SUNY, USA * Jan Otop, IST, Austria * Christophe Ringeissen, LORIA-INRIA Lorraine, France * Manfred Schmidt-Schauss, Goethe-University Frankfurt, Germany * Mateu Villaret, Universitat de Girona, Spain (co-chair) For more information, please contact any of the two chairs Santiago Escobar or Mateu Villaret.

1 1

Contracting Haskell dev role at Standard Chartered
by Don Stewart 28 Jan '15

28 Jan '15

The Strats team at Standard Chartered is hiring a developer for a 1 year contracting role in London. The role is to develop and extend our parsing and validation library for FpML, using the FpML Haskell library to parse and build financial product data into our internal Haskell data types. You will extend our library to support more products, as well as building testing and validation tools (e.g. in QuickCheck) to confirm the soundness and completeness of the implementation. This is a rare entry level Haskell role, and you'll join a very experienced team. More details at: https://donsbot.wordpress.com/2015/01/28/contracting-haskell-development-ro…

1 0

CFP: WPTE 2015 Second International Workshop on Rewriting Techniques for Program Transformations and Evaluation
by David Sabel 27 Jan '15

27 Jan '15

FIRST CALL FOR PAPERS Second International Workshop on Rewriting Techniques for Program Transformations and Evaluation WPTE 2015 affiliated with RDP 2015 2 July, 2015, Warsaw, Poland http://www.trs.cm.is.nagoya-u.ac.jp/event/wpte2015/ Aims and Scope ============== The aim of WPTE is to bring together the researchers working on program transformations, evaluation, and operationally-based programming language semantics, using rewriting methods, in order to share the techniques and recent developments and to exchange ideas to encourage further activation of research in this area. The previous WPTE was held in Vienna 2014. Topics of interest in the scope of this workshop include: * Correctness of program transformations, optimizations and translations. * Program transformations for proving termination, confluence and other properties. * Correctness of evaluation strategies. * Operational semantics of programs, operationally-based program equivalences such as contextual equivalences and bisimulations. * Cost-models for reasoning about the optimizing power of transformations and the costs of evaluation. * Program transformations for verification and theorem proving purposes. * Translation, simulation, equivalence of programs with different formalisms, and evaluation strategies. * Program transformations for applying rewriting techniques to programs in specific programming languages. * Program transformations for program inversions and program synthesis. * Program transformation and evaluation for Haskell and Rewriting. The programming languages of interest include pure, deterministic, impure, nondeterministic, concurrent, parallel languages, and may employ programming paradigms such as functional, logical, typed, imperative, object-oriented, and higher-order. 'Program transformation and evaluation for Haskell and Rewriting' is a new topic of this workshop: equational reasoning and other rewriting techniques for program verification and analysis; lambda calculi and type systems for functional programs and higher-order rewrite systems; rewriting of type expressions in the type checker; rewriting of programs by refactoring tools, optimizers, code generators; execution of programs as a form of graph rewriting (terms with sharing); Template Haskell, generally introducing a rewriting-like macro language into the compilation process; rewriting modulo commonly occurring axioms such as associativity, commutativity, and identity element. Proceedings =========== The WPTE-proceedings will be published in the 'OpenAccess Series in Informatics (OASIcs)' of 'Schloss Dagstuhl Leibniz-Zentrum fuer Informatik' by the workshop day. Extended abstracts on work in progress are not included in the OASIcs proceedings but they will be included in the USB memory which is distributed to the RDP participants. Paper Submissions ================= WPTE accepts two different kinds of contributions: * Full-papers: ------------ Full-papers must represent original work and should be submitted using the OASIcs LaTeX templates. Full-papers should not exceed 12 pages. Accepted papers will be included in the OASIcs proceedings. * Work in progress: ----------------- There will also be a slot for presenting work in progress. An extended abstract of at most 4 pages is required to be submitted using the OASIcs LaTeX templates. These contributions will not be included in the OASIcs proceedings for full-papers but they will be distributed to the workshop participants. One author of each accepted paper or abstract is expected to present it at the workshop. Important Dates =============== * Submission deadline: 17 April 2015 * Notification of acceptance: 15 May 2015 * Deadline for camera-ready proceedings: 29 May 2015 * Workshop: 2 July 2015, Warsaw, Poland Weblinks ======== * EasyChair Submission Website https://www.easychair.org/conferences/?conf=wpte2015 * Homepage of WPTE 2015 http://www.trs.cm.is.nagoya-u.ac.jp/event/wpte2015/ * OASIcs Website (including LaTeX templates): http://www.dagstuhl.de/en/publications/oasics * RDP 2015 http://rdp15.mimuw.edu.pl Program Committee ================= Takahito Aoto (RIEC, Tohoku University) Yuki Chiba (JAIST) Fer-Jan de Vries (University of Leicester) Santiago Escobar (Universitat Politecnica de Valencia) - chair Johan Jeuring (Open Universiteit Nederland and Universiteit Utrecht) Delia Kesner (Universite Paris-Diderot) Serguei Lenglet (Universite de Lorraine) Elena Machkasova (University of Minnesota, Morris) William Mansky (University of Pennsylvania) Joachim Niehren (INRIA Lille) Naoki Nishida (Nagoya University) - chair Kristoffer H Rose (Two Sigma Investments, LLC) Manfred Schmidt-Schauss (Goethe-University Frankfurt am Main) David Sabel (Goethe-University Frankfurt am Main) Masahiko Sakai (Nagoya University) Janis Voigtlaender (University of Bonn) Johannes Waldmann (HTWK Leipzig) Harald Zankl (University of Innsbruck) Organizers ========== Yuki Chiba (JAIST) Santiago Escobar (Universitat Politecnica de Valencia) Naoki Nishida (Nagoya University) - chair Manfred Schmidt-Schauss (Goethe-University Frankfurt am Main) - chair David Sabel (Goethe-University Frankfurt am Main)

1 0

Drastic Prelude changes imminent
by Augustsson, Lennart 27 Jan '15

27 Jan '15

If you didn't know that, e.g., the type of foldr is changing, check out the thread https://www.haskell.org/pipermail/libraries/2015-January/024777.html. This email and any attachments are confidential and may also be privileged. If you are not the intended recipient, please delete all copies and notify the sender immediately. You may wish to refer to the incorporation details of Standard Chartered PLC, Standard Chartered Bank and their subsidiaries at http://www.standardchartered.com/en/incorporation-details.html Insofar as this communication contains any market commentary, the market commentary has been prepared by a sales and/or trading desk of Standard Chartered Bank or its affiliate. It is not and does not constitute research material, independent research, recommendation or financial advice. Any market commentary is for information purpose only and shall not be relied for any other purpose, and is subject to the relevant disclaimers available at http://wholesalebanking.standardchartered.com/en/utility/Pages/d-mkt.aspx. Please visit http://wholesalebanking.standardchartered.com/en/capabilities/financialmark… for important information with respect to derivative products.

2 2

ANN: Halcyon and Haskell on Heroku
by Miëtek Bak 26 Jan '15

26 Jan '15

I’m happy to announce the initial public release of Halcyon, a system for installing Haskell apps and development tools. https://halcyon.sh/ Halcyon stands on the shoulders of Cabal, and isn’t intended to replace it. Instead, consider Halcyon a proof-of-concept implementation of one possible future version of Cabal. - See the Halcyon examples for a demonstration of advanced Halcyon features. https://halcyon.sh/examples/ - Take a look at the Halcyon shootout for a comparison of build times and sizes across most Haskell web frameworks. https://halcyon.sh/shootout/ - Read the Halcyon tutorial to learn how to develop a simple Haskell web app using Halcyon. https://halcyon.sh/tutorial/ While Halcyon isn’t a deployment system, it’s intended to be used for constructing deployment systems. I’m doubly happy to also announce Haskell on Heroku, a buildpack for deploying Haskell apps. https://haskellonheroku.com/ - Read the Haskell on Heroku tutorial to learn how to deploy Haskell web apps to Heroku. https://haskellonheroku.com/tutorial/ Enjoy, -- Miëtek Bak https://mietek.io/

1 0

[ANNOUNCE] New release of SBV
by Levent Erkok 23 Jan '15

23 Jan '15

I'm happy to announce a new release of SBV (v4.0); a library for seamlessly integrating SMT solvers with Haskell. https://hackage.haskell.org/package/sbv Most of the changes in this release are due to Brian Huffman of Galois; essentially adding capabilities so end-users can define symbolic bit-vector types that are not natively supported by SBV. For instance, a user can define `SWord17` for representing 17-bit words and use them just like other symbolic types natively supported by SBV. This feature allows SBV to take advantage of arbitrary bit-size decision procedures for bit-vector logics as found in modern SMT solvers, which are becoming increasingly more valuable in (semi-)automated verification of software artifacts. (Note that SBV already supports other basic types such as unbounded Integers, IEEE Floats and Doubles, Rationals, Algebraic reals, and traditional machine word sizes such as Word8/Int8; 16; 32; and 64 symbolically.) We plan to also add automatic support for SWordN/SIntN for arbitrary N, once GHC gets proper support for type-level naturals. Thanks to Brian Huffman for his contributions to this release. Bug reports/comments are always welcome. -Levent.

1 0

ANN: git-monitor
by John Wiegley 22 Jan '15

22 Jan '15

git-monitor auto-commits all changes to a Git working tree, within a special branch named "refs/snapshots/refs/heads/<branch>". It has no impact on the Git repository otherwise, and will not effect your real branches. It has the following features: - It is designed to be extremely resource efficient, both in CPU cost and memory. I wanted something I could run several instances of on my laptop, without paying much of a battery cost. This efficiency is achieved by using gitlib with the libgit2 backend. The current state of the working tree is maintained as a Git object in memory, and is updated in place before being written back out to disk. Thus, the amount of computation done remains minimal, as we do not need to rebuild the Git tree at each iteration (as "git-commit" would do). - Whenever git-monitor is exited and restarted, the previous snapshot "branch" is discarded. These are only intended to be viable during and between runs. - By having such a branch, you can easily browse through the diffs of your changes throughout the day. By default, every action taken is printed to the console where git-monitor is run, but it can also be run in silent mode, for example if you choose to background it for the rest of the day. http://hackage.haskell.org/package/git-monitor https://github.com/jwiegley/git-monitor Please report issues to the GitHub page. I have been using git-monitor on a regular basis for more than a year now, so I felt it finally deserved an announcement here. Thank you, John Wiegley (johnw on IRC/freenode)

2 2

Haskell Weekly News: Issue 315
by Daniel Santa Cruz 22 Jan '15

22 Jan '15

Welcome to issue 315 of the HWN, an issue covering crowd-sourced bits of information about Haskell from around the web. This issue covers from January 4 to 17, 2015 Quotes of the Week * mpickering: When is the right time to use Data.ByteString.Char8? edwardk: mpickering: some time around 1980 * tpolecat: any lecture by conal elliott has that flavor. he is the bob ross of functional programming. Top Reddit Stories * Write You a Haskell Domain: dev.stephendiehl.com, Score: 280, Comments: 24 Original: [1] http://goo.gl/isSXWc On Reddit: [2] http://goo.gl/kOevyS * Announcing LTS Haskell 1.0 Domain: fpcomplete.com, Score: 87, Comments: 14 Original: [3] http://goo.gl/QW25bK On Reddit: [4] http://goo.gl/PlWgfm * MSFT open sources production serialization system written partially in Haskell Domain: blog.nullspace.io, Score: 83, Comments: 6 Original: [5] http://goo.gl/SDm7i1 On Reddit: [6] http://goo.gl/wljTKD * haskell-emacs - Write Emacs extensions in Haskell Domain: github.com, Score: 64, Comments: 3 Original: [7] http://goo.gl/NkK9FE On Reddit: [8] http://goo.gl/75zURt * The Type Theory Podcast, Episode 3: Dan Licata on Homotopy Type Theory Domain: typetheorypodcast.com, Score: 58, Comments: 17 Original: [9] http://goo.gl/z30wH5 On Reddit: [10] http://goo.gl/5KDPNu * Cabal 1.22 and cabal-install 1.22 Domain: groups.google.com, Score: 54, Comments: 3 Original: [11] http://goo.gl/WdxPu0 On Reddit: [12] http://goo.gl/ih07XV * [Haskell-cafe] The amount of CPP we have to use is getting out of hand Domain: haskell.org, Score: 51, Comments: 94 Original: [13] http://goo.gl/0OYZ7C On Reddit: [14] http://goo.gl/4QCAIc * Boston Haskell lightning talks: Rust, Phantoms, ATS, Freezing, Music, and Code reuse Domain: self.haskell, Score: 50, Comments: 8 Original: [15] http://goo.gl/TAjkMi On Reddit: [16] http://goo.gl/TAjkMi * Haskell for all: total-1.0.0: Exhaustive pattern matching using traversals, prisms, and lenses Domain: haskellforall.com, Score: 47, Comments: 9 Original: [17] http://goo.gl/TJDioE On Reddit: [18] http://goo.gl/sx7aMu * Mutation analysis for Haskell (alpha) Domain: self.haskell, Score: 46, Comments: 9 Original: [19] http://goo.gl/MByMzL On Reddit: [20] http://goo.gl/MByMzL * Simple Algebraic Data Types by Bartosz Milewski Domain: bartoszmilewski.com, Score: 45, Comments: 1 Original: [21] http://goo.gl/Ns3UjL On Reddit: [22] http://goo.gl/uuqCt2 * The Frank programming language Domain: homepages.inf.ed.ac.uk, Score: 42, Comments: 29 Original: [23] http://goo.gl/msxrp5 On Reddit: [24] http://goo.gl/0NPQYY * GHC Weekly News - 2015/01/07 Domain: ghc.haskell.org, Score: 42, Comments: 3 Original: [25] http://goo.gl/HVsDLU On Reddit: [26] http://goo.gl/JiMf4b * The Rust community grapples with the menace of ORPHAN INSTANCES Domain: discuss.rust-lang.org, Score: 42, Comments: 19 Original: [27] http://goo.gl/HIl68S On Reddit: [28] http://goo.gl/dUWa48 * The state and future of supercompilation in GHC. Domain: self.haskell, Score: 39, Comments: 10 Original: [29] http://goo.gl/e9FDLV On Reddit: [30] http://goo.gl/e9FDLV Top StackOverflow Questions * Implementation of null function votes: 18, answers: 2 Read on SO: [31] http://goo.gl/cVqJa3 * What is the type of this self-applying factorial function? votes: 17, answers: 3 Read on SO: [32] http://goo.gl/vQaeQ0 * Haskell fast concurrent queue votes: 17, answers: 3 Read on SO: [33] http://goo.gl/HdAlul * Ghc: partially compile Haskell code? votes: 13, answers: 1 Read on SO: [34] http://goo.gl/hS2QNQ * What is the type of return 5 in Haskell when no context is given? votes: 12, answers: 1 Read on SO: [35] http://goo.gl/IC08Sk * Is it possible to write fmap for this data type involving a type family? votes: 11, answers: 1 Read on SO: [36] http://goo.gl/6V5Mps * How to get cabal and nix work together votes: 11, answers: 1 Read on SO: [37] http://goo.gl/TOXNDv * What is the most general way to compute the depth of a tree with something like a fold? votes: 8, answers: 2 Read on SO: [38] http://goo.gl/vlcioF * What is exactly an indexed functor in Haskell and what are its usages? votes: 8, answers: 1 Read on SO: [39] http://goo.gl/10PK8U * Functor instance for generic polymorphic ADTs in Haskell? votes: 8, answers: 2 Read on SO: [40] http://goo.gl/Oh0uFp * Finite State Transducers in Haskell? votes: 7, answers: 1 Read on SO: [41] http://goo.gl/gu80ZL * Is it possible to encode a generic “lift” function in Haskell? votes: 7, answers: 2 Read on SO: [42] http://goo.gl/R9B8N5 * Haskell Expression Equivalents votes: 6, answers: 1 Read on SO: [43] http://goo.gl/t54YiS Until next time, [44]+Daniel Santa Cruz References 1. http://dev.stephendiehl.com/fun/ 2. http://www.reddit.com/r/haskell/comments/2regln/write_you_a_haskell/ 3. https://www.fpcomplete.com/blog/2015/01/announcing-lts-haskell-1-0 4. http://www.reddit.com/r/haskell/comments/2rapgt/announcing_lts_haskell_10/ 5. http://blog.nullspace.io/bond-oss.html 6. http://www.reddit.com/r/haskell/comments/2rxkmk/msft_open_sources_productio… 7. https://github.com/knupfer/haskell-emacs 8. http://www.reddit.com/r/haskell/comments/2sdvyu/haskellemacs_write_emacs_ex… 9. http://typetheorypodcast.com/2015/01/episode-3-dan-licata-on-homotopy-type-… 10. http://www.reddit.com/r/haskell/comments/2rnumy/the_type_theory_podcast_epi… 11. https://groups.google.com/forum/#!msg/haskell-cafe/rRbP9oJjOBc/J8lf_sGVl_oJ 12. http://www.reddit.com/r/haskell/comments/2rcuak/cabal_122_and_cabalinstall_… 13. https://www.haskell.org/pipermail/haskell-cafe/2015-January/117683.html 14. http://www.reddit.com/r/haskell/comments/2shv2d/haskellcafe_the_amount_of_c… 15. http://www.reddit.com/r/haskell/comments/2sn8la/boston_haskell_lightning_ta… 16. http://www.reddit.com/r/haskell/comments/2sn8la/boston_haskell_lightning_ta… 17. http://www.haskellforall.com/2015/01/total-100-exhaustive-pattern-matching.… 18. http://www.reddit.com/r/haskell/comments/2s1tfx/haskell_for_all_total100_ex… 19. http://www.reddit.com/r/haskell/comments/2rj5sw/mutation_analysis_for_haske… 20. http://www.reddit.com/r/haskell/comments/2rj5sw/mutation_analysis_for_haske… 21. http://bartoszmilewski.com/2015/01/13/simple-algebraic-data-types/ 22. http://www.reddit.com/r/haskell/comments/2sbl93/simple_algebraic_data_types… 23. http://homepages.inf.ed.ac.uk/slindley/papers/frankly-draft-march2014.pdf 24. http://www.reddit.com/r/haskell/comments/2rao0t/the_frank_programming_langu… 25. https://ghc.haskell.org/trac/ghc/blog/weekly20150107 26. http://www.reddit.com/r/haskell/comments/2rq6zc/ghc_weekly_news_20150107/ 27. http://discuss.rust-lang.org/t/orphan-rules/1322/4 28. http://www.reddit.com/r/haskell/comments/2shyfj/the_rust_community_grapples… 29. http://www.reddit.com/r/haskell/comments/2s97d0/the_state_and_future_of_sup… 30. http://www.reddit.com/r/haskell/comments/2s97d0/the_state_and_future_of_sup… 31. http://stackoverflow.com/questions/27941690/implementation-of-null-function 32. http://stackoverflow.com/questions/27814714/what-is-the-type-of-this-self-a… 33. http://stackoverflow.com/questions/27933941/haskell-fast-concurrent-queue 34. http://stackoverflow.com/questions/27780282/ghc-partially-compile-haskell-c… 35. http://stackoverflow.com/questions/27932794/what-is-the-type-of-return-5-in… 36. http://stackoverflow.com/questions/27936725/is-it-possible-to-write-fmap-fo… 37. http://stackoverflow.com/questions/27968909/how-to-get-cabal-and-nix-work-t… 38. http://stackoverflow.com/questions/27769688/what-is-the-most-general-way-to… 39. http://stackoverflow.com/questions/27771474/what-is-exactly-an-indexed-func… 40. http://stackoverflow.com/questions/27856974/functor-instance-for-generic-po… 41. http://stackoverflow.com/questions/27997155/finite-state-transducers-in-has… 42. http://stackoverflow.com/questions/28003135/is-it-possible-to-encode-a-gene… 43. http://stackoverflow.com/questions/27761821/haskell-expression-equivalents 44. https://plus.google.com/105107667630152149014/about

1 0

AVoCS 2015: First Call for Papers
by YuHui Lin 21 Jan '15

21 Jan '15

--------------------------------------------------------------------- FIRST CALL FOR PAPERS The 15th International Workshop on Automated Verification of Critical Systems AVoCS 2015 1-4 September 2015, Edinburgh, UK https://sites.google.com/site/avocs15/ avocs2015(a)easychair.org --------------------------------------------------------------------- IMPORTANT DATES Submission of abstract (full papers): 5th June 2015 Submission of full papers: 12th June 2015 Notification (full papers): 14th July 2015 Submission of research idea papers: 7th August 2015 Notification (research idea): 14th August 2015 Early registration: 18th August 2015 Submissions of final versions: 21st August 2015 INVITED SPEAKERS Colin O'Halloran (D-RisQ & the University of Oxford) Don Sannella (Contemplate & the University of Edinburgh) SPONSORS Formal Methods Europe (FME) The Scottish Informatics & Computer Science Alliance (SICSA) BACKGROUND The aim of Automated Verification of Critical Systems (AVoCS) 2015 is to contribute to the interaction and exchange of ideas among members of the international research community on tools and techniques for the verification of critical systems. SCOPE The subject is to be interpreted broadly and inclusively. It covers all aspects of automated verification, including model checking, theorem proving, SAT/SMT constraint solving, abstract interpretation, and refinement pertaining to various types of critical systems which need to meet stringent dependability requirements (safety-critical, business-critical, performance-critical, etc.). Contributions that describe different techniques, or industrial case studies are encouraged. The technical programme will consist of invited and contributed talks and also allow for short presentations of research ideas. The workshop will be relatively informal, with an emphasis on discussion where special discussion sessions will be organised around the research ideas presentations. Topics include (but are not limited to): - Model Checking - Automatic and Interactive Theorem Proving - SAT, SMT or Constraint Solving for Verification - Abstract Interpretation - Specification and Refinement - Requirements Capture and Analysis - Verification of Software and Hardware - Specification and Verification of Fault Tolerance and Resilience - Probabilistic and Real-Time Systems - Dependable Systems - Verified System Development - Industrial Applications WORKSHOPS AI4FM 2015: 1 September 2015 -- www.ai4fm.org/ai4fm-2015/ VENUE The event will be held in the International Centre for Mathematical Sciences (ICMS) in the centre of the historic old town of Edinburgh - an UNESCO world heritage site. STUDENT GRANTS Thanks to sponsorships from FME and SICSA we can offer financial support for a limited number of students registering for AVoCS in the form of a registration fee waiver (full or partial). As this is limited, we ask the students that would like to take the advantage of this support to submit a short application. The details on how to apply will be available in due course from the AVoCS webpage. SUBMISSION DETAILS Submissions of full papers to the workshop must not have been published or be concurrently considered for publication elsewhere. All submissions will be peer-reviewed and judged on the basis of originality, contribution to the field, technical and presentation quality, and relevance to the workshop. Submissions are handled via Easychair: https://easychair.org/conferences/?conf=avocs2015 The papers must be written in English and not exceed 15 pages and should use the dedicated AVoCS 2015 EASST template available rom the the following link (for LaTeX and Word): http://journal.ub.tu-berlin.de/eceasst AVoCS also encourages the submissions of research ideas in order to stimulate discussions at the workshop. Reports on ongoing work or surveys on work published elsewhere are welcome. The Programme Committee will select research ideas on the basis of submitted abstracts according to significance and general interest. Research ideas must be written in English and not exceed 2 pages using the EASST template. The presentation of these ideas will be organised around discussions, where the presenter should also prepare a set of question in which the audience will discuss. PROCEEDINGS At the workshop, pre-proceedings will be available in the form of a Heriot-Watt University Technical Report; this report will also include the research ideas. After the workshop, the authors of accepted full papers will have about one month in order to revise their papers for publication in the workshop post- proceedings which will appear in the Electronic Communications of the EASST Open Access Journal. Research ideas will not be part of the proceedings in the Open Access Journal. SPECIAL SCP JOURNAL ISSUE Authors of a selection of the best papers presented at the workshop will be invited to submit extended versions of their work for publication in a special issue of Elsevier's journal Science of Computer Programming. PROGRAM COMMITTEE Ernie Cohen, University of Pennsylvania, USA Ewen Denney, NASA Ames, USA Jean-Christophe Filliatre, CNRS, France Michael Goldsmith, University of Oxford, UK Gudmund Grov, Heriot-Watt University, UK (co-chair) Keijo Heljanko, Aalto University, Finland Mike Hinchey, University of Limerick, Ireland Marieke Huisman, University of Twente, Netherlands Andrew Ireland, Heriot-Watt University, UK (co-chair) Gerwin Klein, NICTA/UNSW, Australia Thierry Lecomte, ClearSy, France Peter Gorm Larsen, Aarhus University, Denmark Panagiotis (Pete) Manolios, Northeastern University, USA Stephan Merz, INRIA Nancy & LORIA, France Jaco van de Pol, University of Twente, Netherlands Markus Roggenbach, Swansea University, UK Marco Roveri, FBK, Italy Thomas Santen, Microsoft Research, Germany Bernard Steffen, Technical University Dortmund, Germany Jan Strejček, Masaryk University, Czech Republic Jun Sun, Singapore University of Technology and Design, Singapore Tayssir Touili, LIAFA, CNRS & University Paris Diderot, France Helen Treharne, University of Surrey, UK Laurent Voisin, Systerel, France Angela Wallenburg, Altran, UK John Wickerson, Imperial College London, UK Peter Ölveczky, University of Oslo, Norway ORGANISERS Gudmund Grov, Heriot-Watt University, UK Andrew Ireland, Heriot-Watt University, UK Yuhui Lin, Heriot-Watt University, UK (Local arrangements and publicity chair) STEERING COMMITTEE Michael Goldsmith, University of Oxford, UK Stephan Merz, INRIA Nancy & LORIA, France Markus Roggenbach, Swansea University, UK ----- We invite research leaders and ambitious early career researchers to join us in leading and driving research in key inter-disciplinary themes. Please see www.hw.ac.uk/researchleaders for further information and how to apply. Heriot-Watt University is a Scottish charity registered under charity number SC000278.

1 0