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

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.

Break

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.

Break

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.

Lunch

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.

Break

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.

Break

GADTs and exhaustiveness: looking for the impossible

Jacques Garrigue and Jacques Le Normand

Important dates

Programme committee

• • Damien Doligez (Inria Paris-Rocquencourt, France)

  • Suresh Jagannathan (Purdue University, USA)

  • Patricia Johann (Appalachian State University, USA)

  • Sam Lindley (University of Edinburgh, UK)

  • Moe Masuko (Ochanomizu University, Japan)

  • Adriaan Moors (Typesafe, USA)

  • Scott Owens (University of Kent, UK)

  • Jonathan Protzenko (Microsoft Research, USA)

  • Martin Sulzmann (Karlsruhe University of Applied Sciences, Germany)

  • Jeremy Yallop (University of Cambridge, UK) (PC chair)

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

• Call for presentations (plain text)

• Call for presentations (HTML)