Higher-order, Typed, Inferred, Strict: ACM SIGPLAN ML Family Workshop
Thursday September 4, 2014, Gothenburg, Sweden
Call For Participation and Program http://okmij.org/ftp/ML/ML14.html
Early registration deadline is August 3. Please register at
https://regmaster4.com/2014conf/ICFP14/register.php
The workshop is conducted in close cooperation with the
OCaml Users and Developers Workshop http://ocaml.org/meetings/ocaml/2014/
taking place on September 5.
*** Program with short summaries ***
(The online version links to the full 2-page abstracts)
* Welcome 09:00
* Session 1: Module Systems 09:10 - 10:00
1ML -- core and modules as one (Or: F-ing first-class modules)
Andreas Rossberg
We propose a redesign of ML in which modules are first-class
values. Functions, functors, and even type constructors are one and
the same construct. Likewise, no distinction is made between
structures, records, or tuples, including tuples over types. Yet,
1ML does not depend on dependent types, and its type structure is
expressible in terms of plain System F-omega, in a minor variation
of our F-ing modules approach. Moreover, it supports (incomplete)
Hindley/Milner-style type inference. Both is enabled by a simple
universe distinction into small and large types.
Type-level module aliases: independent and equal
Jacques Garrigue; Leo White
We promote the use of type-level module aliases, a trivial extension
of the ML module system, which helps avoiding code dependencies, and
provides an alternative to strengthening for type equalities.
* Session 2: Beyond Hindley-Milner 10:30 - 11:20
The Rust Language and Type System (Demo)
Felix Klock; Nicholas Matsakis
Rust is a new programming language for developing reliable and
efficient systems. It is designed to support concurrency and
parallelism in building applications and libraries that take full
advantage of modern hardware. Rust's static type system is safe and
expressive and provides strong guarantees about isolation,
concurrency, and memory safety.
Rust also offers a clear performance model, making it easier to
predict and reason about program efficiency. One important way it
accomplishes this is by allowing fine-grained control over memory
representations, with direct support for stack allocation and
contiguous record storage. The language balances such controls with
the absolute requirement for safety: Rust's type system and runtime
guarantee the absence of data races, buffer overflows, stack
overflows, and accesses to uninitialized or deallocated memory. In
this demonstration, we will briefly review the language features
that Rust leverages to accomplish the above goals, focusing in
particular on Rust's advanced type system, and then show a
collection of concrete examples of program subroutines that are
efficient, easy for programmers to reason about, and maintain the
above safety property.
Doing web-based data analytics with F# (Informed Position)
Tomas Petricek; Don Syme
With type providers that integrate external data directly into the
static type system, F# has become a fantastic language for doing
data analysis. Rather than looking at F# features in isolation, this
paper takes a holistic view and presents the F# approach through a
case study of a simple web-based data analytics platform.
* Session 3: Verification 11:40 - 12:30
Well-typed generic smart-fuzzing for APIs (Experience report)
Thomas Braibant; Jonathan Protzenko; Gabriel Scherer
In spite of recent advances in program certification, testing
remains a widely-used component of the software development cycle.
Various flavors of testing exist: popular ones include unit testing,
which consists in manually crafting test cases for specific parts of
the code base, as well as quickcheck-style testing, where instances
of a type are automatically generated to serve as test inputs.
These classical methods of testing can be thought of as internal
testing: the test routines access the internal representation of the
data structures to be checked. We propose a new method of external
testing where the library only deals with a module interface. The
data structures are exported as abstract types; the testing
framework behaves like regular client code and combines functions
exported by the module to build new elements of the various abstract
types. Any counter-examples are then presented to the
user. Furthermore, we demonstrate that this methodology applies to
the smart-fuzzing of security APIs.
Improving the CakeML Verified ML Compiler
Ramana Kumar; Magnus O. Myreen; Michael Norrish; Scott Owens
The CakeML project comprises a mechanised semantics for a subset of
Standard ML and a formally verified compiler. We will discuss our
plans for improving and applying CakeML in four directions:
optimisations, new primitives, a library, and verified applications.
* Session 4: Implicits 14:00 - 14:50
Implicits in Practice (Demo)
Nada Amin; Tiark Rompf
Popularized by Scala, implicits are a versatile language feature
that are receiving attention from the wider PL community. This demo
will present common use cases and programming patterns with
implicits in Scala.
Modular implicits
Leo White; Frédéric Bour
We propose a system for ad-hoc polymorphism in OCaml based on using
modules as type-directed implicit parameters.
* Session 5: To the bare metal 15:10 - 16:00
Metaprogramming with ML modules in the MirageOS (Experience report)
Anil Madhavapeddy; Thomas Gazagnaire; David Scott; Richard Mortier
In this talk, we will go through how MirageOS lets the programmer
build modular operating system components using a combination of
functors and metaprogramming to ensure portability across both Unix
and Xen, while preserving a usable developer workflow.
Compiling SML# with LLVM: a Challenge of Implementing ML on a Common
Compiler Infrastructure
Katsuhiro Ueno; Atsushi Ohori
We report on an LLVM backend of SML#. This development provides
detailed accounts of implementing functional language
functionalities in a common compiler infrastructure developed mainly
for imperative languages. We also describe techniques to compile
SML#'s elaborated features including separate compilation with
polymorphism, and SML#'s unboxed data representation.
* Session 6: No longer foreign 16:30 - 18:00
A Simple and Practical Linear Algebra Library Interface with Static
Size Checking (Experience report)
Akinori Abe; Eijiro Sumii
While advanced type systems--specifically, dependent types on
natural numbers--can statically ensure consistency among the sizes
of collections such as lists and arrays, such type systems generally
require non-trivial changes to existing languages and application
programs, or tricky type-level programming. We have developed a
linear algebra library interface that guarantees consistency (with
respect to dimensions) of matrix (and vector) operations by using
generative phantom types as fresh identifiers for statically
checking the equality of sizes (i.e., dimensions). This interface
has three attractive features in particular. (i) It can be
implemented only using fairly standard ML types and its module
system. Indeed, we implemented the interface in OCaml (without
significant extensions like GADTs) as a wrapper for an existing
library. (ii) For most high-level operations on matrices (e.g.,
addition and multiplication), the consistency of sizes is verified
statically. (Certain low-level operations, like accesses to
elements by indices, need dynamic checks.) (iii) Application
programs in a traditional linear algebra library can be easily
migrated to our interface. Most of the required changes can be made
mechanically. To evaluate the usability of our interface, we ported
to it a practical machine learning library (OCaml-GPR) from an
existing linear algebra library (Lacaml), thereby ensuring the
consistency of sizes.
SML3d: 3D Graphics for Standard ML (Demo)
John Reppy
The SML3d system is a collection of libraries designed to support
real-time 3D graphics programming in Standard ML (SML). This paper
gives an overview of the system and briefly highlights some of the
more interesting aspects of its design and implementation.
* Poster presentation, at the joint poster session with the OCaml workshop
Nullable Type Inference
Michel Mauny; Benoit Vaugon
We present a type system for nullable types in an ML-like
programming language. We start with a simple system, presented as an
algorithm, whose interest is to introduce the formalism that we
use. We then extend it as system using subtyping constraints, that
accepts more programs. We state the usual properties for both
systems. This is work in progress.
Program Committee
Kenichi Asai Ochanomizu University, Japan
Matthew Fluet Rochester Institute of Technology, USA
Jacques Garrigue Nagoya University, Japan
Dave Herman Mozilla, USA
Stefan Holdermans Vector Fabrics, Netherlands
Oleg Kiselyov (Chair) University of Tsukuba, Japan
Keiko Nakata Tallinn University of Technology, Estonia
Didier Remy INRIA Paris-Rocquencourt, France
Zhong Shao Yale University, USA
Hongwei Xi Boston University, USA
--
Caml-list mailing list. Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs
Subscribe to:
Post Comments (Atom)
No comments:
Post a Comment