ICFP 2021
Sun 22 - Sat 28 August 2021

ML is a large family of programming languages that includes Standard ML, OCaml, F#, CakeML, SML#, Manticore, MetaOCaml, JoCaml, Alice ML, Dependent ML, Flow Caml, Reason ML, and many others. All ML languages, besides a great deal of syntax, share several fundamental traits. They are all higher-order, mostly pure, and typed, with algebraic and other data types. Their type systems inherit from Hindley-Milner. The development of these languages has inspired a large amount of computer science research and influenced many programming languages, including Haskell, Scala, Rust, Clojure, and many others.

ML workshops have been held in affiliation with ICFP continuously since 2005. 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, modern operating system and network services, platform services – build, document, test, deploy) and theoretical (fancy types, module systems, metaprogramming, etc.) 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 Haskell, Scala, Rust, Nemerle, Links, Koka, F*, Eff, 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.

The ML workshop will be a virtual workshop this year.

News

  • March 22nd Excited to announce that Don Syme (Microsoft) will be giving this year’s opening keynote, about the history of the F# programming language

Please contact the PC chair (Jonathan Protzenko) with any questions.

Dates
You're viewing the program in a time zone which is different from your device's time zone - change time zone

Thu 26 Aug

Displayed time zone: Seoul change

18:00 - 19:30
Semantics & VerificationML at ML
Chair(s): Martin Elsman University of Copenhagen, Denmark
18:00
30m
Talk
Composing UNIX with Effect Handlers: A Case Study in Effect Handler Oriented Programming
ML
Daniel Hillerström The University of Edinburgh
Pre-print Media Attached
18:30
30m
Talk
Cameleer: a Deductive Verification Tool for OCaml
ML
Mário Pereira NOVA LINCS & DI -- Nova School of Science and Technology, Antonio Ravara Department of Informatics, Faculty of Sciences and Technology, NOVA University of Lisbon and NOVA LINCS
File Attached
19:00
30m
Talk
Hobbit: A Tool for Contextual Equivalence Checking Using Bisimulation Up-to Techniques
ML
Vasileios Koutavas Trinity College Dublin, Yu-Yang Lin Trinity College Dublin, Nikos Tzevelekos Queen Mary University of London
File Attached
20:00 - 21:30
Compiler & Language CorrectnessML at ML
Chair(s): Robert Atkey University of Strathclyde
20:00
30m
Talk
Formalizing OCaml GADT typing in Coq
ML
Jacques Garrigue Nagoya University, Xuanrui Qi Nagoya University
Pre-print File Attached
20:30
30m
Talk
Demo Paper : Coqlex, an approach to generate verified lexers
ML
Wendlasida Ouedraogo Siemens Mobility & Inria Saclay, Danko Ilik Siemens Mobility, Lutz Strassburger Inria Saclay & LIX, Ecole Polytechnique
Media Attached File Attached
21:00
30m
Talk
Code Extraction from Coq to ML-like languages
ML
Danil Annenkov Concordium Blockchain Research Center, Aarhus University, Mikkel Milo Concordium Blockchain Research Center, Aarhus University, Bas Spitters Aarhus University
Link to publication File Attached
22:00 - 23:30
KeynoteML at ML
22:00
60m
Keynote
Keynote: Narratives and Lessons from The Early History of F#
ML
Don Syme Microsoft
23:30 - 01:00
Language & Library DesignML at ML
Chair(s): Benoît Montagu Inria
23:30
30m
Talk
A metalanguage for multi-phase modularity
ML
Jonathan Sterling Carnegie Mellon University, Robert Harper Carnegie Mellon University, USA
File Attached
00:00
30m
Talk
Unfolding ML datatype declarations without loops
ML
Nicolas Chataing ENS Paris, Gabriel Scherer INRIA Saclay
Pre-print Media Attached
00:30
30m
Talk
Verifying Multiparty Communication Protocols using ML Type Systems
ML
Keigo Imai Gifu University, Rumyana Neykova Brunel University London, Nobuko Yoshida Imperial College London, Shoji Yuen Nagoya University
File Attached

Call for Presentations

Format

The ML 2021 workshop will continue the informal approach followed since 2010. Presentations are selected by the program committee from submitted abstracts. There are no published proceedings, so contributions may be submitted for publication elsewhere. We expect research presentations of original and novel work, but emphasize that rigorous descriptions do not prevent preliminary or surprising work: we hope to encourage exciting (if unpolished) research and deliver a lively workshop atmosphere.

Each presentation should take 20-25 minutes, except demos, which should take 10-15 minutes. The exact time will be decided based on the number of accepted submissions. The presentations will likely be recorded.

Due to the COVID-19 pandemic, the workshop will take place online.

Scope

We seek research presentations on topics including (but not limited to):

  • Language design: abstraction, higher forms of polymorphism, concurrency, distribution and mobility, staging, extensions for semi-structured data, generic programming, object systems, etc.
  • Implementation: compilers, interpreters, type checkers, partial evaluators, runtime systems, garbage collectors, foreign function interfaces, etc.
  • Type systems: inference, effects, modules, contracts, specifications and assertions, dynamic typing, error reporting, etc.
  • Applications: case studies, experience reports, pearls, etc.
  • Environments: libraries, tools, editors, debuggers, cross-language interoperability, functional data structures, etc.
  • Semantics: operational and denotational semantics, program equivalence, parametricity, mechanization, etc.

Four kinds of submissions will be accepted: Research Presentations, Experience Reports, Demos, and Informed Positions.

  • Research Presentations: Research presentations should describe new ideas, experimental results, or significant advances in ML-related projects. We especially encourage presentations that describe work in progress, that outline a future research agenda, or that encourage lively discussion. These presentations should be structured in a way which can be, at least in part, of interest to (advanced) users.
  • Experience Reports: Users are invited to submit Experience Reports about their use of ML and related languages. These presentations do not need to contain original research but they should tell an interesting story to researchers or other advanced users, such as an innovative or unexpected use of advanced features or a description of the challenges they are facing or attempting to solve.
  • Demos: Live demonstrations or short tutorials should show new developments, interesting prototypes, or work in progress, in the form of tools, libraries, or applications built on or related to ML and related languages. (You will need to provide all the hardware and software required for your demo; the workshop organisers are only able to provide a projector.)
  • Informed Positions: A justified argument for or against a language feature. The argument must be substantiated, either theoretically (e.g. by a demonstration of (un)soundness, an inference algorithm, a complexity analysis), empirically or by substantial experience. Personal experience is accepted as justification so long as it is extensive and illustrated with concrete examples.

Important dates:

  • Thursday May 27th: Abstract submission deadline
  • Thursday June 18th: Author notification
  • Thursday August 26th (tentative): ML Family Workshop

Submission details

Submissions should be between one and three pages long, in PDF format, and printable on US Letter or A4 sized paper. The submission should have a short abstract and a body between 0 and 3 pages, in one- or two-column layout. The abstract should be suitable for inclusion in the workshop program. The bibliography will not be counted against the page limit. Appendices may be provided, but reviewers will only look at them if they are curious. Similarly, links to an extended presentation of the submitted work may be provided.

Submissions must be uploaded to the workshop submission website before the submission deadline (Thursday May 27th).

Finally, please be aware that the submissions may be made public – in particular, accepted submissions may be made public on the conference website. Do not include confidential information in the submitted PDF.

Coordination with the OCaml Users and Developers Workshop

The OCaml workshop is seen as more practical and is dedicated in significant part to OCaml community building and the development of the OCaml system. In contrast, the ML family workshop is not focused on any language in particular, is more research-oriented, and deals with general issues of ML-style programming and type systems. Yet there is an overlap, which we are keen to explore in various ways. The authors who feel their submission fits both workshops are encouraged to mention it at submission time or contact the program chairs.

Accepted Papers

Title
A Data-centered User Study for jsCoq (short talk)
ML
File Attached
A metalanguage for multi-phase modularity
ML
File Attached
Cameleer: a Deductive Verification Tool for OCaml
ML
File Attached
Code Extraction from Coq to ML-like languages
ML
Link to publication File Attached
Composing UNIX with Effect Handlers: A Case Study in Effect Handler Oriented Programming
ML
Pre-print Media Attached
Demo Paper : Coqlex, an approach to generate verified lexers
ML
Media Attached File Attached
Experience Report: Domain Modeling with F# (short talk)
ML
Media Attached File Attached
Formalizing OCaml GADT typing in Coq
ML
Pre-print File Attached
Frozen inference constraints for type-directed disambiguation
ML
Pre-print Media Attached
Hobbit: A Tool for Contextual Equivalence Checking Using Bisimulation Up-to Techniques
ML
File Attached
Isomorphisms are back! (short talk)
ML
File Attached
Sylvester: Unified, typed, notation for symbolic mathematics and proofs (short talk)
ML
Media Attached File Attached
Unfolding ML datatype declarations without loops
ML
Pre-print Media Attached
Verifying Multiparty Communication Protocols using ML Type Systems
ML
File Attached
Questions? Use the ML contact form.