2014-07-31

[Caml-list] The ML Family workshop: program and the 2nd call for participation

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

2014-07-29

[Caml-list] ETAPS 2015 1st call for papers

******************************************************************

CALL FOR PAPERS: ETAPS 2015

18th European Joint Conferences on Theory And Practice of Software

London, UK, 11-18 April 2015

http://www.etaps.org/2015

******************************************************************

-- ABOUT ETAPS --

ETAPS is the primary European forum for academic and industrial
researchers working on topics relating to software science. ETAPS,
established in 1998, is a confederation of six main annual
conferences, accompanied by satellite workshops. ETAPS 2015 is the
eighteenth event in the series.


-- MAIN CONFERENCES (13-17 April) --

* CC: Compiler Construction
(PC chair Björn Franke, University of Edinburgh, UK)
* ESOP: European Symposium on Programming
(PC chair Jan Vitek, Northeastern University, USA)
* FASE: Fundamental Approaches to Software Engineering
(PC chairs Alexander Egyed, Johannes Kepler U Linz, Austria,
and Ina Schaefer, Technische Universität Braunschweig, Germany)
* FOSSACS: Foundations of Software Science
and Computation Structures
(PC chair Andrew Pitts, University of Cambridge, UK)
* POST: Principles of Security and Trust
(PC chairs Riccardo Focardi, Università Ca' Foscari Venezia,
Italy, and Andrew Myers, Cornell University, USA)
* TACAS: Tools and Algorithms for
the Construction and Analysis of Systems
(PC chairs Christel Baier, Technische Univ Dresden, Germany,
and Cesare Tinelli, The University of Iowa, USA)

TACAS '14 will host the 4rd Competition on Software Verification
(SV-COMP).


-- INVITED SPEAKERS --

* Unifying speakers:
Robert Harper (Carnegie Mellon University, USA)
Catuscia Palamidessi (INRIA Saclay and LIX, France)

* CC invited speaker:
Keshav Pingali (University of Texas, USA)
* FoSSaCS invited speaker:
Frank Pfenning (Carnegie Mellon University, USA)
* TACAS invited speaker:
Wang Yi (Uppsala Universitet, Sweden)


-- IMPORTANT DATES --

* 10 October 2014: Submission deadline for abstracts
* 17 October 2014: Submission deadline for full papers
* 3-5 December 2014: Author response period (ESOP and FoSSaCS only)
* 19 December 2014: Notification of acceptance
* 16 January 2015: Camera-ready versions due


-- SUBMISSION INSTRUCTIONS --

ETAPS conferences accept two types of contributions: research papers
and tool demonstration papers. Both types will appear in the
proceedings and have presentations during the conference.

ESOP and FoSSaCS accept only research papers. TACAS has more paper
categories (see http://www.etaps.org/2015/tacas).

A condition of submission is that, if the submission is accepted, one
of the authors attends the conference to give the presentation.

Submitted papers must be in English presenting original
research. They must be unpublished and not submitted for publication
elsewhere. In particular, simultaneous submission of the same
contribution to multiple ETAPS conferences is forbidden. The
proceedings will be published in the Advanced Research in Computing
and Software Science (ARCoSS) subline of Springer's Lecture Notes in
Computer Science series.

Papers must follow the formatting guidelines specified by Springer at

http://www.springer.de/comp/lncs/authors.html

and be submitted electronically in pdf through the EasyChair author
interface of the respective conference (HotCRP for ESOP).

Submissions not adhering to the specified format and length may be
rejected immediately.


- Research papers

FASE, FOSSACS and TACAS have a page limit of 15 pages for research
papers, whereas CC, POST allow at most 20 pages and ESOP 25 pages.

Additional material intended for the referees but not for publication
in the final version - for example, details of proofs - may be placed
in a clearly marked appendix that is not included in the page
limit. ETAPS referees are at liberty to ignore appendices and papers
must be understandable without them.

In addition to regular research papers, TACAS solicits also case study
papers (at most 15 pages).

Both TACAS and FASE solicit also regular tool papers (at most 15
pages).


- Tool demonstration papers

Submissions should consist of two parts:

* The first part, at most 4 pages, should describe the tool
presented. Please include the URL of the tool (if available) and
provide information that illustrates the maturity and robustness of
the tool. (This part will be included in the proceedings.)

* The second part, at most 6 pages, should explain how the
demonstration will be carried out and what it will show, including
screen dumps and examples. (This part will be not be included in the
proceedings, but will be evaluated.

ESOP and FOSSACS do not accept tool demonstration papers.

TACAS has a page limit of 6 pages for tool demonstrations.


-- SATELLITE EVENTS (11-12 April, 18 April) --

Around 20 satellite workshops will take place before and after the
main conferences.


-- HOST CITY --

London, the capital city of England and the UK, is a leading global
city, with strengths in the arts, commerce, education, entertainment,
fashion, finance, healthcare, media, professional services, research
and development, tourism and transport all contributing to its
prominence. It is one of the world's leading financial centers and a
world cultural capital. It is the world's most-visited city as
measured by international arrivals and has the world's largest city
airport system measured by passenger traffic. In 2012, London became
the first city to host the modern Summer Olympic Games three times.


-- HOST INSTITUTION --

ETAPS 2015 is hosted by the School of Electrical Engineering and
Computer Science of the Queen Mary University of London.

The main campus is located in the Mile End area of the East End of
London.


-- ORGANIZERS

* General chairs: Pasquale Malacaria, Nikos Tzevelekos
* Workshops chair: Paulo Oliva


-- FURTHER INFORMATION --

Please do not hesitate to contact the organizers at
p.malacaria@qmul.ac.uk, nikos.tzevelekos@qmul.ac.uk.


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

2014-07-27

[Caml-list] PPDP 2014: Program and 2nd Call for Participation

======================================================================

CALL FOR PARTICIPATION:

PPDP 2014
16th International Symposium on
Principles and Practice of Declarative Programming
Canterbury, Kent, September 8-10, 2014
http://users-cs.au.dk/danvy/ppdp14/

co-located with

LOPSTR 2014
24th International Symposium on
Logic-Based Program Synthesis and Transformation
Canterbury, Kent, September 9-11, 2014
http://www.iasi.cnr.it/events/lopstr14/

======================================================================

Two weeks left for early registration (until August 8):
http://www.cs.kent.ac.uk/events/2014/ppdp-lopstr-14/

A significant discount is available when registering to both events,
especially as a student (until August 8).

PPDP 2014 features
* an invited talk by Roberto Giacobazzi, shared with LOPSTR:
"Obscuring Code -- Unveiling and Veiling Information in Programs"
* no fewer than 4 distilled tutorials by
- Henrik Nilsson and Ivan Perez:
"Declarative Game Programming"
- Danko Ilik:
"Proofs in Continuation-Passing Style:
normalization of Gödel's System T extended with sums and
delimited control operators"
- Jerzy Karczmarczuk:
"On the Declarative Structure of Quantum Concepts:
States and Observables"
- Ralf Laemmel, Andrei Varanovich, and Martin Leinberger:
"Declarative Software Development"
* the most influential paper 10-year award for PPDP 2004


Tentative program:

==========

Monday 8 September

Welcome to PPDP 2014 - 08:45-09:00
Olaf Chitil and Andy King

Distilled Tutorial - 9:00-10:00
Ralf Laemmel
"Declarative Software Development"

Break - 10:00-10:15

Session - 10:15-11:15

10:15-10:45
Rémi Douence and Nicolas Tabareau
"Lazier Imperative Programming"

10:45-11:15
Stefan Mehner, Daniel Seidel, Lutz Straßburger and Janis Voigtländer
"Parametricity and Proving Free Theorems for Functional-Logic Languages"

Break - 11:15-11:30

Session - 11:30-12:30

11:30:-12:00
Paul Tarau
"Bijective Collection Encodings and Boolean Operations
with Hereditarily Binary Natural Numbers"

12:00-12:30
Flavio Cruz, Ricardo Rocha and Seth Goldstein
"Design and implementation of a multithreaded virtual machine
for executing linear logic programs"

Lunch break - 12:30-14:00

Distilled tutorial - 14:00-15:00
Danko Ilik
"Proofs in Continuation-Passing Style:
normalization of Gödel's System T
extended with sums and delimited control operators"

Break - 15:00-15:15

Session - 15:15-16:15

15:15-15:45
Kenichi Asai, Luminous Fennell, Peter Thiemann and Yang Zhang
"A Type Theoretic Specification for Partial Evaluation"

15:45-16:15
Paul Downen, Luke Maurer, Zena Ariola and Daniele Varacca
"Continuations, Processes, and Sharing"

Break - 16:15-16:30

Session - 16:30-17:30

16:30-17:00
Pierre Neron
"Partial Inlining for Program Transformation"

17:00-17:30
Jean-Louis Giavitto and José Echeveste
"Real-Time Matching of Antescofo Temporal Patterns"

Program-chair report - 17:30-17:45
Olivier Danvy

----------

Tuesday 9 September

Distilled tutorial - 9:00-10:00
Jerzy Karczmarczuk
"On the Declarative Structure of Quantum Concepts:
States and Observables"

Break - 10:00-10:15

Session - 10:15-11:15

10:15-10:45
José Meseguer and Salvador Lucas
"Proving Operational Termination of Declarative Programs in General
Logics"

10:45-11:15
Fan Yang, Santiago Escobar, Catherine Meadows, José Meseguer and
Paliath Narendran
"Theories of Homomorphic Encryption, Unification, and the Finite
Variant Property"

Break - 11:15-11:30

Session - 11:30-12:30

11:30:-12:00
Tzu-Chun Chen, Mariangiola Dezani-Ciancaglini and Nobuko Yoshida
"On the Preciseness of Subtyping in Session Types"

12:00-12:30
Hugo Pacheco, Tao Zan and Zhenjiang Hu
"BiFluX: A Bidirectional Functional Update Language for XML"

Lunch break - 12:30-14:00

Distilled tutorial - 14:00-15:00
Henrik Nilsson
"Declarative Game Programming"

Break - 15:00-15:15

Session - 15:15-16:15

15:15-15:45
Francisco Ferreira and Brigitte Pientka
"Bidirectional Elaboration of Dependently Typed Programs"

15:45-16:15
Steven Ramsay
"Exact Intersection Type Abstractions for Safety Checking of
Recursion Schemes"

Break - 16:15-16:30

Session - 16:30-17:30

16:30-17:00
Julian Kranz and Axel Simon
"Structure-Preserving Compilation:
Efficient Integration of Functional DSLs into Legacy Systems"

17:00-17:30
Ulrich Schöpp
"Organising Low-Level Programs using Higher Types"

----------

Wednesday 10 September

Invited talk - 9:00-10:00
Roberto Giacobazzi
Obscuring Code -- Unveiling and Veiling Information in Programs

Break - 10:00-10:15

Session - 10:15-11:15

10:15-10:45
Rémy Haemmerlé
"On Combining Backward and Forward Chaining in Constraint Logic
Programming"

10:45-11:15
Nataliia Stulova, Jose F. Morales and Manuel V. Hermenegildo
"Assertion-based Debugging of Higher-Order (C)LP Programs"

Break - 11:15-11:30

Session - 11:30-12:30

11:30:-12:00
Takahito Aoto and Sorin Stratulat
"Decision Procedures for Proving Inductive Theorems without Induction"

12:00-12:30
Joachim Jansen, Ingmar Dasseville, Jo Devriendt and Gerda Janssens
"Experimental Evaluation of a State-of-the-Art Grounder"

Lunch break - 12:30-13:30

Session - 13:30-14:30

13:30:-14:00
Tom Schrijvers, Nicolas Wu, Benoit Desouter and Bart Demoen
"Heuristics entwined with handlers combined"

14:00-14:30
James Cheney, Amal Ahmed and Umut Acar
"Database queries that explain their work"

==========

Also, please note a change of dates: LOPSTR will start on September 9,
rather than September 10 as previously announced.

See you in Canterbury!

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

2014-07-25

[Caml-list] Call for participation: Functional High-Performance Computing (FHPC) 2014

The 3rd ACM SIGPLAN Workshop on Functional High Performance Computing
(FHPC 2014) will be held in Gothenburg on September 4 (immediately after
ICFP).

FHPC features exciting talks about a range of topics: optimizing
compilation, GPU computing, computing on heterogeneous platforms, as
well as parallel applications and programming patterns.
It will be a very enjoyable workshop so please consider attending.

The full workshop programme is available at
https://sites.google.com/site/fhpcworkshops/fhpc-2014/programme

Registration for FHPC is done using the ICFP registration site.

Online registration for both ICFP and FHPC starts here:
https://regmaster4.com/2014/ICFP14/ic01code/regsystem.php?control=register

Note that the last day for early registration at ICFP and associated
workshops is August 3!

With best wishes
Mary Sheeran, Ryan Newton, and Jost Berthold

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

2014-07-12

[Caml-list] PPDP 2014 Call for Participation

======================================================================

CALL FOR PARTICIPATION:

PPDP 2014
16th International Symposium on
Principles and Practice of Declarative Programming
Canterbury, Kent, September 8-10, 2014
http://users-cs.au.dk/danvy/ppdp14/

co-located with

LOPSTR 2014
24th International Symposium on
Logic-Based Program Synthesis and Transformation
Canterbury, Kent, September 9-11, 2014
http://www.iasi.cnr.it/events/lopstr14/

======================================================================

Registration is now open:
http://www.cs.kent.ac.uk/events/2014/ppdp-lopstr-14/

A significant discount is available when registering to both events,
especially as a student (until August 8).

PPDP 2014 features
* an invited talk by Roberto Giacobazzi, shared with LOPSTR:
"Obscuring Code -- Unveiling and Veiling Information in Programs"
* no fewer than 4 distilled tutorials by
- Henrik Nilsson and Ivan Perez:
"Declarative Game Programming"
- Danko Ilik:
"Proofs in Continuation-Passing Style:
normalization of Gödel's System T extended with sums and
delimited control operators"
- Jerzy Karczmarczuk:
"On the Declarative Structure of Quantum Concepts:
States and Observables"
- Ralf Laemmel, Andrei Varanovich, and Martin Leinberger:
"Declarative Software Development"
* a rich program of 22 contributed research talks
* the most influential paper 10-year award for PPDP 2004

Also, please note a change of dates: LOPSTR will start on September 9,
rather than September 10 as previously announced.

Hope to see you in Canterbury.


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

2014-07-07

[Caml-list] ML Family workshop: First Call for Participation

Higher-order, Typed, Inferred, Strict: ACM SIGPLAN ML Family Workshop
Thursday September 4, 2014, Gothenburg, Sweden

Call For Participation http://okmij.org/ftp/ML/ML14.html

Early registration deadline is August 3. Please register at
https://regmaster4.com/2014conf/ICFP14/register.php

This workshop specifically aims to recognize the entire extended ML
family and to provide the forum to present and discuss common issues,
both practical (compilation techniques, implementations of concurrency
and parallelism, programming for the Web) and theoretical (fancy
types, module systems, metaprogramming). We also encourage
presentations from related languages (such as Scala, Rust, Nemerle,
ATS, etc.), to exchange experience of further developing ML ideas.

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

* Andreas Rossberg
1ML -- core and modules as one (Or: F-ing first-class modules)

* Jacques Garrigue and Leo White
Type-level module aliases: independent and equal

* Felix Klock and Nicholas Matsakis
Demo: The Rust Language and Type System

* Tomas Petricek and Don Syme
Doing web-based data analytics with F#

* Thomas Braibant, Jonathan Protzenko and Gabriel Scherer
Well-typed generic smart-fuzzing for APIs

* Ramana Kumar, Magnus O. Myreen, Michael Norrish and Scott Owens
Improving the CakeML Verified ML Compiler

* Leo White and Frederic Bour
Modular implicits

* Nada Amin and Tiark Rompf
Implicits in Practice

* Anil Madhavapeddy, Thomas Gazagnaire, David Scott and Richard Mortier
Metaprogramming with ML modules in the MirageOS

* Katsuhiro Ueno and Atsushi Ohori
Compiling SML# with LLVM: a Challenge of Implementing ML on a Common
Compiler Infrastructure

* Akinori Abe and Eijiro Sumii
A Simple and Practical Linear Algebra Library Interface
with Static Size Checking

* John Reppy
SML3d: 3D Graphics for Standard ML


In addition, the joint poster session with the OCaml workshop will take
place in the afternoon on September 5. The session will include
posters:

* Nicolas Oury
Core.Sequence: a unified interface for sequences

* Thomas Gazagnaire, Amir Chaudhry, Anil Madhavapeddy, Richard Mortier,
David Scott, David Sheets, Gregory Tsipenyuk, Jon Crowcroft
Irminsule: a branch-consistent distributed library database

* Michel Mauny and Benoit Vaugon
Nullable Type Inference

* Edwin Toeroek
LibreS3: design, challenges, and steps toward reusable libraries

* Fabrice Le Fessant
A Case for Multi-Switch Constraints in OPAM


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

2014-07-04

[Caml-list] OCaml 2014 Call for Participation

Dear Camlers,

We have now a preliminary program for OCaml 2014,
co-located with ICFP 2014 in Gothenburg, on September 5.

We invite you to register for the workshop from the ICFP site:
http://icfpconference.org/icfp2014/

You can find the up-to-date program at: http://ocaml.org/meetings/ocaml/2014/
Note that this year we are working in close cooperation with the
ML Family workshop: http://okmij.org/ftp/ML/ML14.html

Jacques Garrigue
-----

OCaml 2014 - Preliminary Program

09:00-09:10 - Welcome

09:10-10:00 - Runtime system

Multicore OCaml, by Stephen Dolan, Leo White, Anil Madhavapeddy (University of Cambridge)

Ephemerons meet OCaml GC, by François Bobot (CEA)

10:25-11:20 - Tools and libraries

Introduction to 0install, by Thomas Leonard (University of Cambridge)

Transport Layer Security purely in OCaml (*), by Hannes Mehnert (University of Cambridge), David Kaloper Meršinjak (University of Nottingham)

OCamlOScope: a New OCaml API Search (*), by Jun Furuse (Standard Chartered Bank, Singapore)

11:40-12:30 - OCaml News

The State of OCaml (invited), Xavier Leroy (INRIA Paris-Rocquencourt)

The OCaml Platform v1.0, by Anil Madhavapeddy (C), Amir Chaudhry (C), Jeremie Diminio (JS), Thomas Gazagnaire (C), Louis Gesbert (OCamlPro), Thomas Leonard (C), David Sheets (C), Mark Shinwell (JS), Leo White (C), Jeremy Yallop (C); (C = University of Cambridge, JS = Jane Street).

12:30-14:00 - Lunch

14:00-14:55 - Language

A Proposal for Non-Intrusive Namespaces in OCaml, by Pierrick Couderc (I), Fabrice Le Fessant (I+O), Benjamin Canou (O), Pierre Chambart (O); (I = INRIA, O = OCamlPro)

Improving Type Error Messages in OCaml (*), by Arthur Charguéraud (INRIA & Université Paris Sud)

Github Pull Requests for OCaml development: a field report (*), by Gabriel Scherer (INRIA)

15:10-16:30 - Joint Poster Session (with ML Family workshop)

Core.Sequence: a unified interface for sequences, by Nicolas Oury (Jane Street)

Irminsule; a branch-consistent distributed library database, by Thomas Gazagnaire (C), Amir Chaudhry (C), Anil Madhavapeddy (C), Richard Mortier (University of Nottingham), David Scott (Citrix System), David Sheets (C), Gregory Tsipenyuk (C), Jon Crowcroft (C); (C = University of Cambridge)

A Case for Multi-Switch Constraints in OPAM, by Fabrice Le Fessant (INRIA)

LibreS3: design, challenges, and steps toward reusable libraries, by Edwin Török (Skylable Ltd.)

Nullable Type Inference, by Michel Mauny and Benoit Vaugon (ENSTA-ParisTech)

16:30-17:50 - Applications

Coq of OCaml, by Guillaume Claret (Université Paris Diderot)

High Performance Client-Side Web Programming with SPOC and Js of ocaml (*), by Mathias Bourgoin and Emmmanuel Chailloux (Université Pierre et Marie Curie)

Using Preferences to Tame your Package Manager, Roberto Di Cosmo (D+I), Pietro Abate (D), Stefano Zacchiroli (D), Fabrice Le Fessant (I), Louis Gesbert (OCamlPro); (D = Université Paris Diderot, I = INRIA)

Simple, efficient, sound-and-complete combinator parsing for all context-free grammars, using an oracle (*), by Tom Ridge (University of Leicester)

17:50 - Closing

(*) short presentation


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