2016
Thursday September 22, 2016, Nara, Japan
(immediately following ICFP and preceding OCaml Users and Developers Workshop)
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 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, Scala and Clojure, Rust, ATS and many others.
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 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.
Final Program
9:10-9:15 Welcome
9:15-10:15 Invited Talk
Making Reactive Programs Function
Neelakantan Krishnaswami
The ML family of programming languages is best known as a family of functional programming languages, but most ML-family languages also offer support for effects such as control operators and state. Indeed, they usually support full first-class general references, which can contain values of any type, including higher types. Concretely, programmers may store functions that can modify the heap, within the heap itself.
Since higher-order imperative programs are often much more difficult to understand than programs using either higher-order or imperative features alone, programmers are encouraged to stick to the functional fragment much as possible. However, one place where higher-order state is used quite heavily in practice is in interactive programs, like graphical user interfaces. These reactive systems are typically implemented in an aggressively higher-order stateful style, with each mutable component storing a set of callbacks to invoke whenever a particular event happens.
In this talk, I will describe a recent line of work on structuring these kinds of programs, based on the idea of using a Curry-Howard proof term correspondence with temporal logic as a type system for reactive programs. One of the surprises of this line of work is how many of the standard implementation techniques for reactive programs turn out to realize fundamental logical primitives. This opens the door to reactive programming models which retain both the simple reasoning principles of functional programming, and the efficient implementation strategies known to working programmers.
10:15-10:35 Break
10:35-11:25 Web
WebAssembly: high speed at low cost for everyone
Andreas Rossberg
WebAssembly is a new language- and platform-independent binary code format bringing native-code performance to the web. We present its design and report our experience with specifying its semantics via a reference interpreter written in OCaml, that currently serves as a proxy for a future formal specification.
Extracting from F* to C: a progress report
Peng Wang, Karthikeyan Bhargavan, Jean-Karim Zinzindohoué, Abhishek Anand,
Cédric Fournet, Bryan Parno, Jonathan Protzenko, Aseem Rastogi, and Nikhil Swamy
F* is a language in the tradition of ML equipped with dependent types, monadic effects, refinement types and a weakest precondition calculus. Together, these features enable the F* programmer to prove functional correctness using a combination of automation via SMT solving and manual program proofs.
In the context of the greater Everest project, we are using F* to prove, build and deploy miTLS, a verified, efficient implementation of the Transport Layer Security (TLS) 1.3 protocol.
This extended abstract presents our work in progress. We are currently focusing our efforts on proving the memory safety and functional correctness of Elliptic Curve Cryptography (ECC) primitives, and on extracting this code to C. ECC primitives are a good candidate: they are modeled after the reference implementations in C. Therefore, they only exercise an imperative, first-order subset of F* that lends itself well to an efficient extraction to C.
11:25-11:45 Break
11:45-12:25 Implementation
Compiling with Continuations and LLVM
Kavon Farvardin and John Reppy
This paper describes a new LLVM-based backend for the Parallel ML compiler (part of the Manticore system). This backend is novel in that it supports heap-allocated first-class continuations (a first for LLVM), which, in turn enables language features, such as callcc, lightweight concurrency mechanisms, and PML’s parallelism features.
Tomohiro Sasaki, Katsuhiro Ueno, and Atsushi Ohori
This paper reports on the extension of SML# with natural join operator commonly used in database query. The extension is based on the database typing of Ohori and Buneman and an HM(X)-style constraint polymorphic typing. Based on this typing and type inference algorithm, the seamless SQL integration of SML# is extended with natural join. The extended SML# is available as a version 3.1.0-trial_join.
12:25-14:00 Lunch
14:00-14:50 Effects
Oleg Kiselyov and Kc Sivaramakrishnan
We present the embedding of the language Eff into OCaml, using the library of delimited continuations or the OCaml-effects branch. The embedding is systematic, lightweight, performant and supports even higher-order, `dynamic’ effects with their polymorphism. OCaml thus may be regarded as another implementation of Eff, broadening the scope and appeal of that language.
Compiling Links Effect Handlers to the OCaml Backend
Daniel Hillerström, Sam Lindley, and Kc Sivaramakrishnan
Algebraic effects and handlers provide a modular abstraction for modeling and controlling computational effects. We present a compiler for the experimental language Links with effect handlers. Our compiler interfaces with the Multicore OCaml backend to take advantage of OCaml's implementation of efficient handlers.
14:50-15:20 Break
15:20-16:10 Classes
Claudio Russo, Matthew Windsor, Don Syme, Rupert Horlick, and James Clarke
Type classes are an immensely popular and productive feature of Haskell. They have since been adopted in, and adapted to, numerous other languages, including theorem provers. This talk will show that type classes have a natural and efficient representation in .NET. This paves the way for the extension of F# and other .NET languages with Haskell style type classes. The representation is type preserving and promises easy and safe cross-language inter-operation. We are currently, and rapidly, extending the open source C# compiler and language service, Roslyn, with support for type classes but intend to do the same for F# once that work has been completed.
Close Encounters of the Higher Kind - Emulating Constructor Classes in Standard ML
Yutaka Nagashima and Liam O'Connor
We implement a library for encoding constructor classes in Standard ML, including elaboration from minimal definitions, and automatic instantiation of superclasses.
16:10-16:40 Break
16:40-17:35 Future
Stephen Dolan
Malfunction is an untyped program representation intended as a compilation target for functional languages, consisting of a thin wrapper around OCaml's Lambda intermediate representation.
Compilers targeting Malfunction convert programs to a simple s-expression-based syntax with clear semantics, which is then compiled to native code using OCaml's back-end, enjoying both the optimisations of OCaml's new flambda pass, and its battle-tested runtime and garbage collector.
Gabriel Scherer, Luc Maranget, and Thomas Réfis
The or-pattern (p | q) matches a value v if either p or q match v. It may happen that both p and q match certain values, but that they don't bind their variables at the same places. OCaml specifies that the left pattern p then takes precedence, but users intuitively expect an angelic behavior, making the ``best'' choice. Subtle bugs arise from this mismatch. When are (p | q) and (q | p) observably different?
To correctly answer this question we had to go back to pattern matrices, the primary technique to compile patterns and analyze them for exhaustivity, redundant clauses, etc. There is a generational gap: pattern matching was actively studied when most ML languages were first implemented, but many of today's students and practitioners trust our elders to maintain and improve them. Read on for your decadely fix of pattern matching theory!
Typed Embedding of Relational Language in OCaml
Dmitri Kosarev and Dmitri Boulytchev
We present an implementation of relational programming language miniKanren as a set of combinators and syntax extension for OCaml. The key feature of our approach is polymorphic unification, which can be used to unify data structures of almost arbitrary types. In addition we provide a useful generic programming pattern to systematically develop relational specifications in a typed manner, and address the problem of relational and functional code integration.
The following paper will be presented in the OCaml workshop (September 23rd):
Sundials/ML: interfacing with numerical solvers
Timothy Bourke, Jun Inoue, and Marc Pouzet
We describe a comprehensive OCaml interface to the Sundials suite of numerical solvers (version 2.6.2). Noteworthy features include the treatment of the central vector data structure and benchmarking results.
Important dates
Friday 10th 20th June (any time zone)
Monday 18th July
Abstract submission deadline
Author notification
Thursday 22nd September 2016
ML Family Workshop
Invited Speaker
We are happy to announce the invited speaker for ML 2016:
Neelakantan Krishnaswami (University of Cambridge, UK)
Programme committee
Nada Amin (EPFL, Switzerland)
Kenichi Asai (Ochanomizu University, Japan) (PC chair)
Jacques Carette (McMaster University, Canada)
Arthur Charguéraud (INRIA, France)
Yan Chen (Google, USA)
Jan Midtgaard (Technical University of Denmark, Denmark)
John Reppy (University of Chicago, USA)
Mark Shinwell (Jane Street Europe, UK)
Nikhil Swamy (Microsoft Research, USA)
Katsuhiro Ueno (Tohoku University, Japan)
Steering Committee
Kenichi Asai, Ochanomizu University, Japan (PC chair 2016)
Jeremy Yallop, Cambridge University, UK (PC chair 2015)
Oleg Kiselyov, Monterey, CA, USA (PC chair 2014)
Daan Leijen, Microsoft Research, Redmond, USA (PC chair 2013)
Didier Remy, INRIA, France (member-at-large since Nov. 2015)
Jacques Garrigue, Nagoya University, Japan (member-at-large since Nov. 2014)
John Reppy, University of Chicago, USA (member-at-large since Aug. 2014)