Higher-order, Typed, Inferred, Strict: ACM SIGPLAN ML Family Workshop

Thursday August 26, 2021, virtual

(immediately following ICFP and preceding OCaml Users and Developers Workshop)

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.

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

If you have any question about the workshop, submission or participation, feel free to send them by email to the program chair, Jonathan Protzenko.

Important dates

  • Thursday May 27th: Abstract submission deadline

  • Thursday June 18th: Author notification

  • Thursday August 26th (tentative): ML Family Workshop


  • Composing UNIX with Effect Handlers: A Case Study in Effect Handler Oriented Programming (Daniel Hillerström The University of Edinburgh)

  • Cameleer: a Deductive Verification Tool for OCaml (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)

  • Hobbit: A Tool for Contextual Equivalence Checking Using Bisimulation Up-to Techniques (Vasileios Koutavas Trinity College Dublin, Yu-Yang Lin Trinity College Dublin, Nikos Tzevelekos Queen Mary University of London)

  • Formalizing OCaml GADT typing in Coq (Jacques Garrigue Nagoya University, Xuanrui Qi Nagoya University)

  • Demo Paper : Coqlex, an approach to generate verified lexers (Wendlasida Ouedraogo Siemens Mobility & Inria Saclay, Danko Ilik Siemens Mobility, Lutz Strassburger Inria Saclay & LIX, Ecole Polytechnique)

  • Code Extraction from Coq to ML-like languages (Danil Annenkov Concordium Blockchain Research Center, Aarhus University, Mikkel Milo Concordium Blockchain Research Center, Aarhus University, Bas Spitters Aarhus University)

  • A metalanguage for multi-phase modularity (Jonathan Sterling Carnegie Mellon University, Robert Harper Carnegie Mellon University, USA)

  • Unfolding ML datatype declarations without loops (Nicolas Chataing ENS Paris, Gabriel Scherer INRIA Saclay)

  • Verifying Multiparty Communication Protocols using ML Type Systems (Keigo Imai Gifu University, Rumyana Neykova Brunel University London, Nobuko Yoshida Imperial College London, Shoji Yuen Nagoya University)

  • Frozen inference constraints for type-directed disambiguation (Olivier Martinot INRIA, Gabriel Scherer INRIA Saclay)

  • Experience Report: Domain Modeling with F# (short talk) (Scott Wlaschin None)

  • Isomorphisms are back! (short talk) (Clément Allain Inria, Gabriel Radanne Inria, Laure Gonnord University of Lyon & LIP, France)

  • Sylvester: Unified, typed, notation for symbolic mathematics and proofs (short talk) (Allister Beharry None)

  • A Data-centered User Study for jsCoq (short talk) (Hanneli Tavante McGill University)

Programme committee

    • Danel Ahman (University of Ljubljana)

    • Robert Atkey (University of Strathclyde)

    • Frédéric Bour (Tarides)

    • Ezgi Çiçek (Facebook London)

    • Youyou Cong (Tokyo Institute of Technology)

    • Richard A. Eisenberg (Tweag I/O)

    • Martin Elsman (University of Copenhagen, Denmark)

    • Ohad Kammar (University of Edinburgh)

    • Naoki Kobayashi (University of Tokyo, Japan)

    • Benoît Montagu (Inria)

    • Jonathan Protzenko (Microsoft Research) (Chair)

    • Kristina Sojakova (INRIA Paris)

    • Don Syme (Microsoft)

    • Matías Toro (University of Chile)

    • Katsuhiro Ueno (Tohoku University)