[TYPES/announce] Final CFP: ML Family Workshop 2017

[Sam Lindley]

----------------------------------------------------------------------
                           CALL FOR PAPERS

                       ML Family Workshop 2017
                     7 September 2017, Oxford, UK

                   http://www.mlworkshop.org/ml2017/
                        (co-located with ICFP)
----------------------------------------------------------------------

ML is a 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 share several fundamental
traits, besides a good deal of syntax. They are higher-order, strict,
mostly pure, and typed, with algebraic and other data types. Their
type systems are derived from Hindley-Milner. The development of these
languages has inspired a significant body of computer science research
and influenced the design of many other programming languages,
including Haskell, Rust, and Scala.

ML workshops have been held in affiliation with ICFP continuously
since 2005. This workshop specifically aims to recognise the entire
extended ML family and to provide a forum for presenting and
discussing 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 ATS, Eff, F*, Koka,
Links, Rust, Scala, Swift, etc.), to exchange experience of further
developing ML ideas. Last year's ML Family workshop included talks
covering eight different ML dialects and related languages: Eff, F#,
F*, Links, Manticore, OCaml, SML, and SML#.

The ML family workshop will be held in close coordination with the
OCaml Users and Developers Workshop.

Invited speaker
---------------

Edwin Brady (University of St Andrews, UK)

   State machines all the way down

   A useful pattern in dependently typed programming is to define
   a state transition system, for example the states and
   operations in a network protocol, as an indexed monad. We index
   each operation by its input and output states, thus
   guaranteeing that operations satisfy pre- and post-conditions,
   by typechecking. However, what if we want to write a program
   using several systems at once? What if we want to define a high
   level state transition system, such as a network application
   protocol, in terms of lower level states, such as network
   sockets and mutable variables?

   In this talk, I will present an architecture for dependently
   typed applications based on a hierarchy of state transition
   systems, implemented in a generic data type ST. This is based
   on a monad indexed by contexts of resources, allowing us to
   reason about multiple state transition systems in the type of a
   function. Using ST, we show: how to implement a state
   transition system as a dependent type, with type level
   guarantees on its operations; how to account for operations
   which could fail; how to combine state transition systems into
   a larger system; and, how to implement larger systems as a
   hierarchy of state transition systems. I will illustrate the
   system with a high level network application protocol,
   implemented in terms of POSIX network sockets.

Scope
-----

We acknowledge the whole breadth of the ML family and aim to include
languages that are closely related, such as Rust and Scala. 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 state of the art ML might
favourably influence those related languages. Specifically, we seek
research presentations on topics including (but not limited to):

   * Language design: abstraction, higher forms of polymorphism,
     concurrency, distribution and mobility, staging, extensions for
     semi-structured data, generic programming, object systems, etc.

   * Implementation: compilers, interpreters, type checkers, partial
     evaluators, runtime systems, garbage collectors, foreign function
     interfaces, etc.

   * Type systems: inference, effects, 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.

   * Semantics: operational and denotational semantics, program
     equivalence, parametricity, mechanization, etc.

Four kinds of submissions will be accepted: Research Presentations,
Experience Reports, Demos and Informed Positions.

   * 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 and related languages. (You will need to provide all the
     hardware and software required for your demo; the workshop
     organisers are only able to provide a projector.)

   * 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 substantial
     experience. Personal experience is accepted as justification so
     long as it is extensive and illustrated with concrete examples.

Format
------

The ML 2017 workshop will continue the informal approach followed
since 2010. Presentations are selected from submitted abstracts. There
are no published proceedings, so contributions may be submitted for
publication elsewhere. We hope that this format will encourage 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-proceedings
----------------

ML 2017 is an informal workshop without proceedings. We are planning
to publish a post-proceedings and to invite interested authors of
selected presentations to expand their abstracts for inclusion.

Coordination with the OCaml Users and Developers Workshop
---------------------------------------------------------

The OCaml workshop is seen as more practical and is dedicated in
significant part to OCaml community building and the development 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 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 programme chairs.

Submission details
------------------

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
programme. The bibliography will not be counted against the page
limit.

Submissions must be uploaded to the workshop submission website

   https://icfp-mlworkshop17.hotcrp.com/

before the submission deadline (Wednesday 31st May). If you have a
question concerning the scope of the workshop or the submission
process, please contact the programme chair.

Important dates
---------------

Wednesday 31st May (any time zone)  Abstract submission deadline
Wednesday 28th June                 Author notification
Thursday 7th September 2017         ML Family Workshop

Programme committee
-------------------

Nick Benton (Facebook, UK)
Małgorzata Biernacka (University of Wroclaw, Poland)
Stephen Dolan (University of Cambridge, UK)
Shin-ya Katsumata (Kyoto University, Japan)
Julia Lawall (LIP6 Paris, France)
Sam Lindley (The University of Edinburgh, UK) (PC chair)
Andreas Rossberg (Google, Germany)
Sukyoung Ryu (KAIST, South Korea)
Gabriel Scherer (Northeastern University, US)
Alley Stoughton (Boston University, US)
Niki Vazou (University of Maryland, US)

-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.