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.

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.

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.

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.

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.

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.