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.
|Session 1||Module Systems Chair: Didier Rémy|
|09:10||1ML -- core and modules as one (Or: F-ing first-class modules) (Research presentation)
We propose a redesign of ML in which modules are first-class values. Functions, functors, and even type constructors are one and the same construct. Likewise, no distinction is made between structures, records, or tuples, including tuples over types. Yet, 1ML does not depend on dependent types, and its type structure is expressible in terms of plain System F-omega, in a minor variation of our F-ing modules approach. Moreover, it supports (incomplete) Hindley/Milner-style type inference. Both is enabled by a simple universe distinction into small and large types.
|09:35||Type-level module aliases: independent and equal (Research presentation)
Jacques Garrigue (Nagoya University); Leo White (University of Cambridge)
We promote the use of type-level module aliases, a trivial extension of the ML module system, which helps avoiding code dependencies, and provides an alternative to strengthening for type equalities.
|10:00 - 10:30||coffee break|
|Session 2||Verification Chair: Anil Madhavapeddy|
|10:30||Well-typed generic smart-fuzzing for APIs (Experience report)
Thomas Braibant (Cryptosense); Jonathan Protzenko; Gabriel Scherer (INRIA)
|10:55||Improving the CakeML Verified ML Compiler (Research presentation)
Ramana Kumar; Magnus O. Myreen (University of Cambridge); Michael Norrish (NICTA); Scott Owens (University of Kent)
The CakeML project comprises a mechanised semantics for a subset of Standard ML and a formally verified compiler. We will discuss our plans for improving and applying CakeML in four directions: optimisations, new primitives, a library, and verified applications.
|11:20 - 11:40||break|
|Session 3||Beyond Hindley-Milner Chair: Jacques Garrigue|
|11:40||The Rust Language and Type System (Demo)
Felix Klock; Nicholas Matsakis (Mozilla Research)
Rust is a new programming language for developing reliable and efficient systems. It is designed to support concurrency and parallelism in building applications and libraries that take full advantage of modern hardware. Rust's static type system is safe and expressive and provides strong guarantees about isolation, concurrency, and memory safety.
|12:05||Doing web-based data analytics with F# (Informed Position)
Tomas Petricek (University of Cambridge); Don Syme (Microsoft Research Cambridge)
With type providers that integrate external data directly into the static type system, F# has become a fantastic language for doing data analysis. Rather than looking at F# features in isolation, this paper takes a holistic view and presents the F# approach through a case study of a simple web-based data analytics platform.
|12:30 - 14:00||lunch|
|Session 4||Implicits Chair: Andreas Rossberg|
|14:00||Implicits in Practice (Demo)
Nada Amin (EPFL); Tiark Rompf (EPFL & Oracle Labs)
Popularized by Scala, implicits are a versatile language feature that are receiving attention from the wider PL community. This demo will present common use cases and programming patterns with implicits in Scala.
|14:25||Modular implicits (Research presentation)
Leo White; Frédéric Bour (University of Cambridge)
We propose a system for ad-hoc polymorphism in OCaml based on using modules as type-directed implicit parameters.
|14:50 - 15:10||break|
|Session 5||To the bare metal Chair: Martin Elsman|
|15:10||Metaprogramming with ML modules in the MirageOS (Experience report)
Anil Madhavapeddy; Thomas Gazagnaire (University of Cambridge); David Scott (Citrix Systems R&D); Richard Mortier (University of Nottingham)
In this talk, we will go through how MirageOS lets the programmer build modular operating system components using a combination of functors and metaprogramming to ensure portability across both Unix and Xen, while preserving a usable developer workflow.
|15:35||Compiling SML# with LLVM: a Challenge of Implementing ML on a Common Compiler Infrastructure (Research presentation)
Katsuhiro Ueno; Atsushi Ohori (Tohoku University)
We report on an LLVM backend of SML#. This development provides detailed accounts of implementing functional language functionalities in a common compiler infrastructure developed mainly for imperative languages. We also describe techniques to compile SML#'s elaborated features including separate compilation with polymorphism, and SML#'s unboxed data representation.
|16:00 - 16:30||tea break|
|Session 6||No longer foreign Chair: Oleg Kiselyov|
|16:30||A Simple and Practical Linear Algebra Library Interface with Static Size Checking (Experience report)
Akinori Abe; Eijiro Sumii (Tohoku University)
While advanced type systems--specifically, dependent types on natural numbers--can statically ensure consistency among the sizes of collections such as lists and arrays, such type systems generally require non-trivial changes to existing languages and application programs, or tricky type-level programming. We have developed a linear algebra library interface that guarantees consistency (with respect to dimensions) of matrix (and vector) operations by using generative phantom types as fresh identifiers for statically checking the equality of sizes (i.e., dimensions). This interface has three attractive features in particular.
|16:55||SML3d: 3D Graphics for Standard ML (Demo)
John Reppy (University of Chicago)
The SML3d system is a collection of libraries designed to support real-time 3D graphics programming in Standard ML (SML). This paper gives an overview of the system and briefly highlights some of the more interesting aspects of its design and implementation.
at the joint poster session with the OCaml workshop, Sep 5
|Nullable Type Inference
Michel Mauny; Benoit Vaugon (ENSTA-ParisTech)
We present a type system for nullable types in an ML-like programming language. We start with a simple system, presented as an algorithm, whose interest is to introduce the formalism that we use. We then extend it as system using subtyping constraints, that accepts more programs. We state the usual properties for both systems. This is work in progress.
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.
The post-proceedings of selected papers from the ML Family and the OCaml Users and Developers workshops will be published in the Electronic Proceedings in Theoretical Computer Science. 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 EPTCS standards.
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.
|Kenichi Asai||Ochanomizu University, Japan|
|Matthew Fluet||Rochester Institute of Technology, USA|
|Jacques Garrigue||Nagoya University, Japan|
|Dave Herman||Mozilla, USA|
|Stefan Holdermans||Vector Fabrics, Netherlands|
|Oleg Kiselyov (Chair)||University of Tsukuba, Japan|
|Keiko Nakata||Institute of Cybernetics, Estonia|
|Didier Rémy||INRIA Paris-Rocquencourt, France|
|Zhong Shao||Yale University, USA|
|Hongwei Xi||Boston University, USA|
|Alain Frisch||LexiFi, France|
|Oleg Kiselyov||University of Tsukuba, Japan|
|Daan Leijn||Microsoft Research, Redmond, USA|
|Anil Madhavapeddy||Cambridge University, UK|
|Greg Morrisett||Harvard University, USA|
|Chung-chieh Shan (Chair)||Indiana University, USA|