[Haskell-cafe] The ML Family workshop: program and the 2nd call for participation

[oleg at okmij.org]

Higher-order, Typed, Inferred, Strict: ACM SIGPLAN ML Family Workshop
Thursday September 4, 2014, Gothenburg, Sweden

Call For Participation and Program         http://okmij.org/ftp/ML/ML14.html

Early registration deadline is August 3. Please register at
https://regmaster4.com/2014conf/ICFP14/register.php

The workshop is conducted in close cooperation with the
OCaml Users and Developers Workshop  http://ocaml.org/meetings/ocaml/2014/
taking place on September 5.

*** Program with short summaries  ***
(The online version links to the full 2-page abstracts)

* Welcome 09:00
* Session 1: Module Systems 09:10 - 10:00

1ML -- core and modules as one (Or: F-ing first-class modules)
Andreas Rossberg
  We propose a redesign of ML in which modules are first-class
  values. Functions, functors, and even type constructors are one and
  the same construct. Likewise, no distinction is made between
  structures, records, or tuples, including tuples over types. Yet,
  1ML does not depend on dependent types, and its type structure is
  expressible in terms of plain System F-omega, in a minor variation
  of our F-ing modules approach. Moreover, it supports (incomplete)
  Hindley/Milner-style type inference. Both is enabled by a simple
  universe distinction into small and large types.

Type-level module aliases: independent and equal
Jacques Garrigue; Leo White
  We promote the use of type-level module aliases, a trivial extension
  of the ML module system, which helps avoiding code dependencies, and
  provides an alternative to strengthening for type equalities.

* Session 2: Beyond Hindley-Milner 10:30 - 11:20

The Rust Language and Type System (Demo)
Felix Klock; Nicholas Matsakis
  Rust is a new programming language for developing reliable and
  efficient systems. It is designed to support concurrency and
  parallelism in building applications and libraries that take full
  advantage of modern hardware. Rust's static type system is safe and
  expressive and provides strong guarantees about isolation,
  concurrency, and memory safety.
  Rust also offers a clear performance model, making it easier to
  predict and reason about program efficiency. One important way it
  accomplishes this is by allowing fine-grained control over memory
  representations, with direct support for stack allocation and
  contiguous record storage. The language balances such controls with
  the absolute requirement for safety: Rust's type system and runtime
  guarantee the absence of data races, buffer overflows, stack
  overflows, and accesses to uninitialized or deallocated memory. In
  this demonstration, we will briefly review the language features
  that Rust leverages to accomplish the above goals, focusing in
  particular on Rust's advanced type system, and then show a
  collection of concrete examples of program subroutines that are
  efficient, easy for programmers to reason about, and maintain the
  above safety property.

Doing web-based data analytics with F# (Informed Position)
Tomas Petricek; Don Syme
  With type providers that integrate external data directly into the
  static type system, F# has become a fantastic language for doing
  data analysis. Rather than looking at F# features in isolation, this
  paper takes a holistic view and presents the F# approach through a
  case study of a simple web-based data analytics platform.

* Session 3: Verification 11:40 - 12:30

Well-typed generic smart-fuzzing for APIs (Experience report)
Thomas Braibant; Jonathan Protzenko; Gabriel Scherer
  In spite of recent advances in program certification, testing
  remains a widely-used component of the software development cycle.
  Various flavors of testing exist: popular ones include unit testing,
  which consists in manually crafting test cases for specific parts of
  the code base, as well as quickcheck-style testing, where instances
  of a type are automatically generated to serve as test inputs.
  These classical methods of testing can be thought of as internal
  testing: the test routines access the internal representation of the
  data structures to be checked. We propose a new method of external
  testing where the library only deals with a module interface. The
  data structures are exported as abstract types; the testing
  framework behaves like regular client code and combines functions
  exported by the module to build new elements of the various abstract
  types. Any counter-examples are then presented to the
  user. Furthermore, we demonstrate that this methodology applies to
  the smart-fuzzing of security APIs.

Improving the CakeML Verified ML Compiler
Ramana Kumar; Magnus O. Myreen; Michael Norrish; Scott Owens
  The CakeML project comprises a mechanised semantics for a subset of
  Standard ML and a formally verified compiler. We will discuss our
  plans for improving and applying CakeML in four directions:
  optimisations, new primitives, a library, and verified applications.

* Session 4: Implicits 14:00 - 14:50
        
Implicits in Practice (Demo)
Nada Amin; Tiark Rompf
  Popularized by Scala, implicits are a versatile language feature
  that are receiving attention from the wider PL community. This demo
  will present common use cases and programming patterns with
  implicits in Scala.

Modular implicits
Leo White; Frédéric Bour
  We propose a system for ad-hoc polymorphism in OCaml based on using
  modules as type-directed implicit parameters.

* Session 5: To the bare metal 15:10 - 16:00

Metaprogramming with ML modules in the MirageOS (Experience report)
Anil Madhavapeddy; Thomas Gazagnaire; David Scott; Richard Mortier
  In this talk, we will go through how MirageOS lets the programmer
  build modular operating system components using a combination of
  functors and metaprogramming to ensure portability across both Unix
  and Xen, while preserving a usable developer workflow.

Compiling SML# with LLVM: a Challenge of Implementing ML on a Common
Compiler Infrastructure
Katsuhiro Ueno; Atsushi Ohori
  We report on an LLVM backend of SML#. This development provides
  detailed accounts of implementing functional language
  functionalities in a common compiler infrastructure developed mainly
  for imperative languages. We also describe techniques to compile
  SML#'s elaborated features including separate compilation with
  polymorphism, and SML#'s unboxed data representation.

* Session 6: No longer foreign 16:30 - 18:00

A Simple and Practical Linear Algebra Library Interface with Static
Size Checking (Experience report)
Akinori Abe; Eijiro Sumii
  While advanced type systems--specifically, dependent types on
  natural numbers--can statically ensure consistency among the sizes
  of collections such as lists and arrays, such type systems generally
  require non-trivial changes to existing languages and application
  programs, or tricky type-level programming. We have developed a
  linear algebra library interface that guarantees consistency (with
  respect to dimensions) of matrix (and vector) operations by using
  generative phantom types as fresh identifiers for statically
  checking the equality of sizes (i.e., dimensions).  This interface
  has three attractive features in particular.  (i) It can be
  implemented only using fairly standard ML types and its module
  system. Indeed, we implemented the interface in OCaml (without
  significant extensions like GADTs) as a wrapper for an existing
  library.  (ii) For most high-level operations on matrices (e.g.,
  addition and multiplication), the consistency of sizes is verified
  statically.  (Certain low-level operations, like accesses to
  elements by indices, need dynamic checks.)  (iii) Application
  programs in a traditional linear algebra library can be easily
  migrated to our interface. Most of the required changes can be made
  mechanically.  To evaluate the usability of our interface, we ported
  to it a practical machine learning library (OCaml-GPR) from an
  existing linear algebra library (Lacaml), thereby ensuring the
  consistency of sizes.

SML3d: 3D Graphics for Standard ML (Demo)
John Reppy
  The SML3d system is a collection of libraries designed to support
  real-time 3D graphics programming in Standard ML (SML). This paper
  gives an overview of the system and briefly highlights some of the
  more interesting aspects of its design and implementation.

* Poster presentation, at the joint poster session with the OCaml workshop
Nullable Type Inference
Michel Mauny; Benoit Vaugon
  We present a type system for nullable types in an ML-like
  programming language. We start with a simple system, presented as an
  algorithm, whose interest is to introduce the formalism that we
  use. We then extend it as system using subtyping constraints, that
  accepts more programs. We state the usual properties for both
  systems. This is work in progress.


Program Committee

Kenichi Asai             Ochanomizu University, Japan
Matthew Fluet            Rochester Institute of Technology, USA
Jacques Garrigue         Nagoya University, Japan
Dave Herman              Mozilla, USA
Stefan Holdermans        Vector Fabrics, Netherlands
Oleg Kiselyov (Chair)    University of Tsukuba, Japan
Keiko Nakata             Tallinn University of Technology, Estonia
Didier Remy              INRIA Paris-Rocquencourt, France
Zhong Shao               Yale University, USA
Hongwei Xi               Boston University, USA