ACM SIGPLAN Workshop on ML, September 2015

Higher-order, Typed, Inferred, Strict: ACM SIGPLAN ML Family Workshop

Thursday September 3, 2015, Vancouver, Canada
(immediately following ICFP and preceding OCaml Users and Developers Workshop)

Registration

News


19th August 2015
Abstracts available (Click talk titles to view.)
22nd July 2015
Workshop programme available
14th April 2015
Invited talk by David MacQueen


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.

Programme

0900-1000

The History of Standard ML: Ideas, Principles, Culture (Invited Talk)
David MacQueen

The Standard ML language was created during the 1980s and 1990s in the context of the British, and, more locally, the Edinburgh programming language research community. Here we describe the process of its design and explain how it grew out of previous work by Peter Landin, Christopher Strachey, Rod Burstall, and most directly, Robin Milner and the LCF project. We cover the evolution of important design ideas like polymorphic type inference and algebraic data types, as well as the principles that guided the design, including particularly the role of formal semantics.
1000-1030 Break
1030-1120

Generating code with polymorphic let
Oleg Kiselyov

We practically solve the long-standing vexing problem of generating code with polymorphic let. For polymorphic functions, we rely on a conjecture whose proof will require a re-investigation of the seemingly long-settled value restriction.

Polymorphism, subtyping and type inference in MLsub (slides)
Stephen Dolan and Alan Mycroft

We present a type system combining subtyping and ML-style parametric polymorphism. Unlike previous work, our system supports type inference and infers compact types. We demonstrate this system in the minimal language MLsub, which types a strict superset of core ML programs.
1120-1140 Break
1140-1230

Arduino programming of ML-style in ATS (slides)
Kiwamu Okabe and Hongwei Xi

Functional programming languages often require a large run-time environment supported by the underlying OS to ensure various forms of safety during code execution. For instance, memory safety is usually achieved through systematic garbage collection (GC), which may not be available for embedded programming or should even be avoided on purpose due its adverse effect on predictability. In this talk, we demonstrate that programming in ATS, a language with a functional core of ML-style, can be effectively employed to construct programs running on Arduino Uno (of 2KB SRAM and 8-bit CPU).

Resource monitoring for Poly/ML processes (slides)
David Matthews, Magnus Stenqvist and Tjark Weber

Application monitoring is invaluable to manage the performance of applications, understand their resource requirements and identify bottlenecks. We present a graphical monitoring tool for the Poly/ML run-time system, a popular implementation of Standard ML. This allows to gather and visualize detailed data showing the run-time behavior of Poly/ML applications, and thereby assists developers in understanding and improving the resource needs of such applications.
1230-1400 Lunch
1400-1450

Full dependency and user-defined effects in F* (slides)
Nikhil Swamy, Cătălin Hriţcu, Chantal Keller, Pierre-Yves Strub, Aseem Rastogi, Antoine Delignat-Lavaud, Karthikeyan Bhargavan, and Cédric Fournet

We present (new) F*, a dependently typed, higher-order, strict, effectful language, bringing formal verification to the ML language family. We illustrate the dual uses of F* both as a proof assistant as well as a tool for building and verifying effectful programs. The latest version of F* is programmed in F*, bootstraps in both OCaml and F# on most major platforms, and is open source. We encourage interested ML programmers to gradually migrate critical portions of their programs to F* for verification, while easily and safely interoperating with their existing ML libraries.

Dependent types for real-time constraints (slides)
William Blair and Hongwei Xi

Synchronous programming languages emerged in the 1980s as tools to implement reactive systems. These systems interact with events from their physical environment and often must do so under strict time constraints. In this talk, we use ATS, a statically typed functional language with a highly expressive type system, to support real-time primitives in an experimental synchronous language called Prelude. We show that these primitives and their verification requirements may be expressed using dependent types in ATS, and then modify the Prelude compiler to produce ATS code for type checking. This modified Prelude compiler thus discharges part of its proof obligations to ATS. Whereas ATS is typically used as a general purpose programming language, we want to demonstrate that it can also be used to support certain advanced features in languages equipped with less expressive types.
1450-1510 Break
1510-1600

Manifest contracts for OCaml (slides)
Yuki Nishida and Atsushi Igarashi

We report our work in progress on an extension of the OCaml compiler with a manifest contract system, where contracts are integrated into a type system as "refinement types". Although we aim at hybrid contract checking in future, the current implementation checks all contracts at run time by inserting coercions where they are necessary. We discuss simple use cases of our system, impact on type inference, and a few details of the modified compiler.

Lost in extraction, recovered
Éric Tanter and Nicolas Tabareau

Extracting Coq programs to ML enables a model of software development in which some critical components of a system can be developed in Coq and proven correct, before being extracted to ML and integrated with the rest of the system. However, due to the gap between Coq and ML, key features like properties and type dependencies disappear upon extraction, leading to potentially unsafe and unsound executions of certified components. We describe an approach to protect extracted components through mostly automatic generation of runtime checks, ensuring that the assumptions made by certified components are checked dynamically when interacting with non-certified components.
1600-1630 Break
1630-1655

GADTs and exhaustiveness: looking for the impossible
Jacques Garrigue and Jacques Le Normand

Sound exhaustiveness checking of pattern-matching is an essential feature of GADTs, and OCaml has supported it from day one, by showing that the remaining cases could never be typed. Not only does it allow the programmer to be confident in the soundness of his code, but it also it permits optimizations which make GADTs more efficient. However, while this approach is sound and can prune some simple uses of GADTs, some other uses caused superfluous warnings. In this talk we describe the original approach and how we ensure its soundness, and show that one can do better by turning the type-checking of extra cases into a backtracking proof search algorithm. We also show that the exhaustiveness problem is undecidable for GADTs, so that this proof search must be kept partial.

Important dates

Thursday 3rd September 2015 ML Family Workshop

Programme committee

Steering Committee

  • 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)
  • Alain Frisch (chair), LexiFi, France (PC chair 2012)
  • Jacques Garrigue, Nagoya University, Japan (member-at-large since Nov. 2014)
  • John Reppy, University of Chicago, USA (member-at-large since Aug. 2014)
  • Anil Madhavapeddy, Cambridge University, UK (member-at-large)

Resources

Subpages (1): ML 2015: call for papers
Comments