2015
Thursday September 3, 2015, Vancouver, Canada
(immediately following ICFP and preceding OCaml Users and Developers Workshop)
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
1000-1030
1030-1120
1120-1140
1140-1230
1230-1400
1400-1450
1450-1510
1510-1600
1600-1630
1630-1655
The History of Standard ML: Ideas, Principles, Culture (Invited Talk)
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
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
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.
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.
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
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
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)