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
- 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
|