2023-10-24

[Caml-list] Attn: Development Editor, Latest OCaml Weekly News

OCaml Weekly News

Previous Week Up Next Week

Hello

Here is the latest OCaml Weekly News, for the week of October 17 to 24, 2023.

Ppxlib dev meetings

Sonja Heinze announced

@octachron has come to the ppxlib dev meeting today, which has been a very nice surprise. It’s nice to discuss intersections between ppxlib and the compiler together with compiler maintainers. Thanks, @octachron!

So it has been @panglesd, @octachron and me in the meeting. Here are the meeting notes: https://github.com/ocaml-ppx/ppxlib/wiki/Dev-meeting-19-09-2023.

A hack to implement efficient TLS (thread-local-storage)

Vesa Karvonen announced

Currently OCaml 5 provides a Domain.DLS module for domain-local-state.

Unfortunately,

  1. there is no corresponding Thread.TLS for (sys)thread-local-state, and
  2. the current implementation of Domain.DLS is not thread-safe.

I don’t want to spend time to motivate this topic, but for many of the use cases of Domain.DLS, what you actually want, is to use a Thread.TLS. IOW, many of the uses of Domain.DLS are probably “wrong” and should actually use a Thread.TLS, because, when using Domain.DLS, the assumption must be that you don’t have multiple threads on the domain, but that is typically decided at a higher level in the application and so making such an assumption is typically not safe.

Domain.DLS is not thread-safe

I mentioned that the current implementation Domain.DLS is not thread-safe. What I mean by that is that the current implementation is literally not thread-safe at all in the sense that unrelated concurrent Domain.DLS accesses can actually break the DLS.

Consider the implementation of Domain.DLS.get:

  let get (idx, init) =      let st = maybe_grow idx in      let v = st.(idx) in      if v == unique_value then        let v' = Obj.repr (init ()) in        st.(idx) <- (Sys.opaque_identity v');        Obj.magic v'      else Obj.magic v  

If there are two (or more) threads on a single domain that concurrently call get before init has been called initially, then what might happen is that init gets called twice (or more) and the threads get different values which could e.g. be pointers to two different mutable objects.

Consider the implementation of maybe_grow:

  let maybe_grow idx =      let st = get_dls_state () in      let sz = Array.length st in      if idx < sz then st      else begin        let rec compute_new_size s =          if idx < s then s else compute_new_size (2 * s)        in        let new_sz = compute_new_size sz in        let new_st = Array.make new_sz unique_value in        Array.blit st 0 new_st 0 sz;        set_dls_state new_st;        new_st      end  

Imagine calling get (which calls maybe_grow) with two different keys from two different threads concurrently. The end result might be that two different arrays are allocated and only one of them “wins”. What this means, for example, is that effects of set calls may effectively be undone by concurrent calls of get.

In other words, the Domain.DLS, as it is currently implemented, is not thread-safe.

How to implement an efficient Thread.TLS?

If you dig into the implementation of threads, you will notice that the opaque Thread.t type is actually a heap block (record) of three fields. You can see the Thread.t accessors:

#define Ident(v) Field(v, 0)  #define Start_closure(v) Field(v, 1)  #define Terminated(v) Field(v, 2)  

and the Thread.t allocation:

static value caml_thread_new_descriptor(value clos)  {    CAMLparam1(clos);    CAMLlocal1(mu);    value descr;    /* Create and initialize the termination semaphore */    mu = caml_threadstatus_new();    /* Create a descriptor for the new thread */    descr = caml_alloc_3(0, Val_long(atomic_fetch_add(&thread_next_id, +1)),                         clos, mu);    CAMLreturn(descr);  }  

The second field, Start_closure, is used to pass the closure to the thread start:

static void * caml_thread_start(void * v)  {    caml_thread_t th = (caml_thread_t) v;    int dom_id = th->domain_id;    value clos;    void * signal_stack;      caml_init_domain_self(dom_id);      st_tls_set(caml_thread_key, th);      thread_lock_acquire(dom_id);    restore_runtime_state(th);    signal_stack = caml_init_signal_stack();      clos = Start_closure(Active_thread->descr);    caml_modify(&(Start_closure(Active_thread->descr)), Val_unit);    caml_callback_exn(clos, Val_unit);    caml_thread_stop();    caml_free_signal_stack(signal_stack);    return 0;  }  

and, as seen above, it is overwritten with the unit value before the closure is called.

What this means is that when you call Thread.self () and get a reference to the current Thread.t, the Start_closure field of that heap block will be the unit value:

assert (Obj.field (Obj.repr (Thread.self ())) 1 = Obj.repr ())  

Let’s hijack that field for the purpose of implementing an efficient TLS!

Here is the full hack:

module TLS : sig    type 'a key    val new_key : (unit -> 'a) -> 'a key    val get : 'a key -> 'a    val set : 'a key -> 'a -> unit  end = struct    type 'a key = { index : int; compute : unit -> 'a }      let counter = Atomic.make 0    let unique () = Obj.repr counter      let new_key compute =      let index = Atomic.fetch_and_add counter 1 in      { index; compute }      type t = { _id : int; mutable tls : Obj.t }      let ceil_pow_2_minus_1 n =      let n = n lor (n lsr 1) in      let n = n lor (n lsr 2) in      let n = n lor (n lsr 4) in      let n = n lor (n lsr 8) in      let n = n lor (n lsr 16) in      if Sys.int_size > 32 then n lor (n lsr 32) else n      let[@inline never] grow_tls t before index =      let new_length = ceil_pow_2_minus_1 (index + 1) in      let after = Array.make new_length (unique ()) in      Array.blit before 0 after 0 (Array.length before);      t.tls <- Obj.repr after;      after      let[@inline] get_tls index =      let t = Obj.magic (Thread.self ()) in      let tls = t.tls in      if Obj.is_int tls then grow_tls t [||] index      else        let tls = (Obj.magic tls : Obj.t array) in        if index < Array.length tls then tls else grow_tls t tls index      let get key =      let tls = get_tls key.index in      let value = Array.unsafe_get tls key.index in      if value != unique () then Obj.magic value      else        let value = key.compute () in        Array.unsafe_set tls key.index (Obj.repr (Sys.opaque_identity value));        value      let set key value =      let tls = get_tls key.index in      Array.unsafe_set tls key.index (Obj.repr (Sys.opaque_identity value))  end  

The above achieves about 80% of the performance of Domain.DLS allowing roughly 241M ~TLS.get~s/s (vs 296M ~Domain.DLS.get~s/s) on my laptop.

New Get Started Documentation on OCaml.org

Thibaut Mattio announced

Dear OCaml Community,

On behalf of the OCaml.org team, I’m thrilled to announce the publication of the new Get Started documentation.

It is organised in three stages:

  • Installing OCaml, which guides you through the installation of opam, the initialisation of a switch and the installation of Platform tools.
  • A Tour of OCaml, which walks you through the basics of the OCaml language and invites you to use the top-level to start playing with the language.
  • Your First OCaml Program, which is a bit more practical and assumes you’re using an editor to help you create your first executable using Dune.

In addition to these, you’ll also find introductory guides on the tooling to complement the introduction to the language:

Our goal is to make OCaml.org the best resource to get started with and learn OCaml.

There are still a lot of gaps to fill in the documentation – and we’ll continue to work on these in the coming months – but the Get Started experience is probably the most important part of the documentation to alleviate friction points that discourage new users from adopting OCaml. As such, don’t hesitate to publicise these, but most importantly, let us know your feedback!

Happy reading!

Web Analytics on OCaml.org

Continuing this thread, Thibaut Mattio said

Thanks for the feedback and the participation in the survey!

Seeing that there aren’t major concerns, we’ll be moving forward with a trial of Plausible.

As @avsm said, we plan on self-hosting it on the OCaml.org infrastructure to respect our commitment to not use any third-party service. This means that not only we won’t be collecting any personal data, but even the aggregate data will never leave the OCaml.org infrastructure.

There’s roughly a third of people who are against adding analytics to OCaml.org in the survey above. We strongly believe that Plausible is aligned with our commitment to protect OCaml.org visitors’ privacy, but I’ll echo @avsm in saying that if people believe that this is not the case, I’d love to hear about the specific concerns and ideas for alternatives.

To answer some questions above:

Are you going to give a public access to the Plausible statistics ? Or will it be only for the maintainers i.e. Tarides ?

The analytics dashboard will be public.

Have you considered running a server-side analytics service?

Yes, @JiaeK actually worked on a server-side analytics service as part of her Outreachy internship in 2021 and had made fantastic progress. The WIP dashboard is available at https://ocaml.org/dashboard.

It currently doesn’t collect any data and only logs unique page accesses.

We had planned on building on top of this, but as you can imagine this is a large project, and the OCaml.org team has been prioritising improvements to the site itself.

I found the following to be a good read on the pros and cons of server-side vs client-side analytics: https://plausible.io/blog/server-log-analysis#how-big-of-a-data-gap-is-there-between-server-log-analysis-and-web-analytics

TL;DR for all its benefits, server-side analytics comes with a load of drawbacks and isn’t fundamentally more privacy-friendly than privacy-oriented client-side analytics solution.

That being said, if someone would like to contribute to the Dream analytics dashboard to make it usable as an alternative to other analytics solutions, I’d be more than happy to move towards this! Don’t hesitate to reach out to me or other OCaml.org maintainers about that.

OCaml.org Newsletter: August and September 2023

Thibaut Mattio announced

Welcome to the August and September 2023 edition of the OCaml.org newsletter! This update has been compiled by the OCaml.org team. You can find the previous updates on Discuss.

Our goal is to make OCaml.org the best resource for anyone who wants to get started and be productive in OCaml. The OCaml.org newsletter provides an update on our progress towards that goal and an overview of changes we are working on.

We couldn’t do it without all the amazing OCaml community members who help us review, revise, and create better OCaml documentation. Your feedback enables us to better prioritise our work and make progress towards our goal. Thank you!

These past two months, our priorities were:

  • Learn Area: We’re working towards making OCaml.org a great resource to learn OCaml and discover its ecosystem. We’ve focussed on getting the new Get Started documentation ready for publication, and we started work on a second iteration of the designs for the Learn area.
  • General Improvements: As usual, we also worked on general maintenance and improvements based on user feedback, so we’re highlighting some of our work below.

Learn Area

  • 1. Redesign of the Learn Area

    After completing the first version of the design in July, we started working on a new iteration that is more in line with the current branding of the site. Feedback from the team and users has been extremely positive on the UX (the structure of the new documentation and the layout of the pages), but we felt that the design direction needed to be reconciled with and improve on the existing designs of all pages. Thus, we are revisiting the designs’ UI aspects in both light and dark modes.

    Relevant PRs and Activities:

    • Continued work on Figma UX/UI designs for the new Learn area:
      • Continued overall Learn area UI design
      • Improved dark mode for the home page on mobile and made necessary text amendments
      • Designed mobile views for the search field with an open navigation feature and breadcrumb navigation
      • Worked on updating the design systems to ensure consistency between light and dark variants
    • Continued the implementation of new components for the Learn Area:
  • 2. OCaml Documentation

    Since August, we’ve focused mainly on the “Getting Started” documents, including a guide to installing OCaml, a “tour” of the OCaml language, and a tutorial to create your first project in OCaml.

    Anticipating on our October update, we’ve just published the new Get Started documentation pages! :tada:

    We still encourage community feedback, as we fully expect to iteratively improve these docs in the coming weeks, especially as they will now serve as the primary resource to everyone who wants to get up and running with OCaml.

    Our focus will now shift to filling the gaps in the Language section of the documentation, starting with the Basic Data Types and Functions and Values pages, which are currently in the Community review stage.

    Relevant PRs and Activities:

General Improvements

This month, we’re welcoming 2 new contributors:

and welcome contributions from returning contributors:

Thanks a lot to all the contributors this month! It’s lovely to see more and more people making contributions to the site!

Relevant PRs and Activities:

Release of odoc 2.3.0

Paul-Elliot announced

The odoc team is thrilled to announce the release of odoc 2.3.0! 🎉 This release is the result of almost a year of diligent work since the last major release of odoc 2.2.0, it comes packed with significant new features and improvements!

🌟 Spotlight Features of Odoc 2.3.0

Here are a couple of the new features introduced in Odoc 2.3.0 that we’d like to highlight.

  • 1. Table Support

    Table support is the last addition to the odoc language, and comes with two syntax flavours: a light one, and a heavy one. The light markup is similar to markdown’s markup for table, producing tables that are readable in the source file as well.

    However, this markup has some limitation, since it only allows inline content in cells. It can also be difficult to read and mantain for big tables, without a proper editor support. For this reason, Odoc also provides a “heavy” markup, closer to the html one, with fewer limitations!

    Here is a table in heavy, light, and rendered form:

      {t  Table | support  ------|--------  is    | cool!  }  
      {table  {tr {th Table} {th support}}  {tr {td is} {td cool!}}  }  
    Table support
    is cool!
  • 2. Source Code Rendering

    Source code rendering is an extremely exciting new feature. Not only odoc is now able to generate a rendering of the source files (and source hierarchy) of a project, but it is also able to create direct links from the documentation to the implementation!

    This puts the documentation browsing to a new level, by helping to quickly answer any implementation-related question!

    The source code rendering is also tailored to OCaml, for instance with links from variables to their definition, something missing from traditional html-based source viewing such as github!

    Using this features in odoc’s driver will require some work, but you can already have a preview of the feature by going to the odoc API website, which was built with the feature enabled. For instance, the Odoc_html module is now populated with many Source links, jumping right into the implementation file! Directory pages to browser the implementation are also included :D

🗺️ Background & Roadmap

Before displaying the full changelog, some background on our roadmap and what comes next.

The lack of access to comprehensive documentation for OCaml libraries is one of the biggest pain points reported by the OCaml community, as highlighted in the 2022 OCaml survey (c.f. Q50).

This motivated the odoc and OCaml.org teams to jointly work on a centralised package documentation, that went live in April 2022, as part of the new version of OCaml.org.

With documentation for OCaml libraries readily available on OCaml.org, we now turn our focus on making sure that library authors have the tooling they need to create high-quality documentation.

Our roadmap highlights some features we believe will make the generated documentation significantly better for readers, and documentation-writing much more pleasant and rewarding.

This release is a significant milestone in implementing the features on our roadmap and is the precursor to a series of upcoming releases. Odoc 2.4.0 will follow shortly and will bring support for search. Stay tuned and follow our progress through the OCaml Platform newsletter!

🤝 Join The Mission

While we are dedicated to developing the best tooling to generate and serve documentation on OCaml.org, creating a well-documented library ecosystem can only be a collective effort. Package authors: we’re working hard to give you great tools, but we’ll need all your help to create an ecosystem of well-documented libraries for OCaml!

If you find that writing documentation for your library isn’t as straightforward as you would like, please do share your feedback with us.

2.3.0 Changelog

  • Added
    • Source code rendering (@Julow, @panglesd, @jonludlam #909, #996, #993, #982)
    • Handle tables markup (@panglesd, @gpetiot, #893)
    • Initial support for assets (@trefis, #975)
    • odoc-parser remerged (@jonludlam, #973) This includes table support (@gpetiot, @panglesd, ocaml-doc/odoc-parser#11 ocaml-doc/odoc-parser#14) and delimited code blocks with optional output (@jonludlam, ocaml-doc/odoc-parser#17)
    • Add a tooltip to references with text (@Julow, #945)
    • Add emoji to alerts in CSS (@yawaramin, #928)
    • Add common language in shipped highlightjs (@Julow, #953)
    • Display ’private’ keyword for private type extensions (@gpetiot, #1019)
  • Fixed
    • Fix --hidden not always taken into account (@panglesd, #940)
    • Syntax highlight labels in function arguments (@panglesd, #990)
    • Ensure generated html ends with a newline (@3Rafal, #954)
    • Warn against tags in pages (@Julow, #948)
    • Remove unhelpful ’Unresolved_apply’ errors (@gpetiot, #946)
    • Allow links and references in headings (@EmileTrotignon, @panglesd, #942)
    • Fix rendering of method types (@zoggy, #935)
    • Fix section labelling with submodules (@EmileTrotignon, @panglesd, #931)
    • LaTeX backend fixes (@Octachron, #921 #920)
    • html: Remove extra space in class declarations (@Julow, #936)
    • Fix rendering of unresolved references (@Julow, #957)

Announce Seppo.Social v0.3 and invite thoughts

Marcus Rohrmoser 🌍 announced

Hi all,

I am happy to announce yesterday’s release of v0.3 of #Seppo!, the friendly, sustainable, permacomputing inspired alternative to all those heavy microblog servers. Generously funded by #NLnet https://nlnet.nl/project/Seppo

It’s built to be operated by yourself on commodity shared webspace without requiring much further attention.

Read more at https://seppo.social/en/support/#installation

Changes

  • post notes
  • being subscribed to (aka ’followed’)
  • distribute post to subscribers
  • job queue to do so
  • housekeeping UX (password, profile page, timezone)

Your thoughts are very much appreciated.

Marcus Rohrmoser https://digitalcourage.social/@mro/111261271071034377

P.S.: There will be 🐫 stickers again, soon.

bwd 2.3.0 for backward lists

Favonia announced

I am happy to announce a new version of bwd for backward lists! The new release added init and a few other List functions introduced in OCaml 5.1 (is_empty, find_index, and find_mapi). It also added many inlining annotations.

Backward lists are isomorphic to regular lists but place elements backward. Using a different type for semantically backward lists can avoid bugs such as missing or misusing List.rev or List.rev_append. Our strategy is to keep the elements’ textual order and avoid functions such as List.rev. Initially, this package was created to eliminate bugs in our type checkers, but we have been using it almost everywhere since then. I recommend using bwd if you use list to store anything semantically backward. 😉

More information at https://github.com/RedPRL/ocaml-bwd

Storing credentials to a private OPAM repository

Richard Degenne announced

Welp, 4 years later, I decided to give that whole private OPAM repository thing another shot, and I ended up with something I’m quite proud of, with a private Opam repository, and private packages uploaded to GitLab’s package registries!

https://blog.richarddegenne.fr/2023/10/20/setting-up-a-private-opam-repository-on-gitlab-step-by-step/

OCaml on Windows: the long paths issue

Manas announced

Not very long ago, I managed to solve the long paths issue for OCaml and I want to share how.

While building a large project, I ran into the path issues - Dune would fail with errors saying a certain file present in a long file was not found. Shortening libraries names helped. But what was really needed was manifesting OCaml tools so that they can perform I/O on long paths as described here on MSDN docs.

Guidelines there expect binary artifacts (dll or exe) have to be manifested with something like this

<?xml version="1.0" encoding="utf-8"?>  <application xmlns="urn:schemas-microsoft-com:asm.v3">      <windowsSettings  xmlns:ws2="http://schemas.microsoft.com/SMI/2016/WindowsSettings">          <ws2:longPathAware>true</ws2:longPathAware>      </windowsSettings>  </application>  

Ideally, the application being built is also manifested so.

I use esy as my daily driver for Windows development. I have always found the workflow on Windows with esy reasonable and never stopped using it since I discovered. Over time, I have taken up maintenance of the project too.

OCaml on Windows is practical only with Cygwin. Not because the tools needs a Unix like environment - they have evolved significants over the years since I have been using OCaml on Windows. Cygwin is convenient because of the libraries in the ecosystem - for instance all the native libraries from GNU project. GNU projects are easily built inside Cygwin/MSYS/mingw but not so outside.

I was worried that I’d have to write some gory hack in the compiler to manifest every binary artifact - dune had to be manifested too. There are many ways to embed the manifest with tools windres etc. But fortunately, I found that Mingw already embeds all executables with a default one. It can be found here among the Cygwin projects

I decided to fork the repository and use the manifest MSDN docs recommended. You can find it here This helped me fix my project, but I wanted this for the rest of the community too.

Esy uses a utility called esy-bash which packages the Cygwin environment for the user. We find that users have mostly uniform setups this way. Helps with reproducibility. I decided to tweak esy-bash to package my fork of the windows-default-manifest along with other Cygwin packages. This way OCaml users dont have to worry about the long paths issue anymore.

This has been available since esy 0.7.0. If you’d like to try the latest esy, it is available on NPM and can be installed with npm i -g esy

I’d love to hear your thoughts on this approach. More than happy to contribute a solution like this for opam too.

A Roadmap for the OCaml Platform - Seeking Your Feedback

Thibaut Mattio announced

I updated the roadmap to incorporate the latest feedback. This update:

  • Adds a workflow to support Dune plugins (W15)
  • Adds a workflow to integrate with other build systems (W16)
  • Adds a workflow to compile to WebAssembly from Dune (W14)
  • Adds a workflow to compile MirageOS unikernels from Dune (W12)
  • Updates Literate Programming workflow to use odoc and mention interactive code blocks (W24)
  • Updates Generate Documentation workflow to list features planned as part of the odoc roadmap (W25)
  • Updates Package Publication to remove mention that users need not to commit an opam file (W26)

A big thank you to everyone who participated in the discussion! Building a community-driven roadmap is no trivial exercise, but witnessing so many people being driven to share constructive feedback, there’s no doubt that it’s absolutely worth it.

Much of the feedback, both here and in other Discuss threads (e.g. https://discuss.ocaml.org/t/the-ocaml-platform-a-vehement-dissent/13008), points out the roadmap’s pronounced Dune-focus. I want to be very clear that while the focus of the coming years highlighted in the roadmap is indeed to consolidate the integration of the Platform tools to create a cohesive experience – a top request in the OCaml surveys – there’s no intention to make Dune the singular solution for OCaml tooling. The OCaml Platform is a collection of independent tools that can be used without Dune, and this will remain the case.

We’ve worked on formalising the Guiding Principles before sharing the roadmap. One key principle we’ve asserted is that while Platform tools operate under a single frontend (the editor or Dune at the moment), they remain independent. @xavierleroy rightly suggested that we commit to this in stronger terms, so we’ve updated the relevant Principle to make this more explicit.

In addition to clarifying the Guiding Principles, seeing that the majority of the feedback we received is asking for better support for non-Dune users, two of the added workflows in this last update (W15 and W16) aim at bringing better support for third-party (i.e. non-Platform) tools.

Special thanks to @jbeckford for initiating discussions on Dune plugins!

Let us know what you think of these new workflows and the other updates! As usual, let’s give an additional 2 weeks for feedback on the roadmap. Barring significant concerns, we’ll undergo a final revision based on all the discussions before adopting the first version.

PS: thank you @shonfeder for pointing out that the issues were deactivated on the repository. I’ve activated them, so don’t hesitate to open issues there now.

Adding Dynamic Arrays / Vectors to StdLib

Continuing this thread, gasche announced

Hi everyone,

A short note: we eventually manage to build consensus on https://github.com/ocaml/ocaml/pull/11882 and I merged it yesterday, so there will be a Dynarray module in the standard library in OCaml 5.2. Thanks @BastouP411 and @c-cube for their efforts bringing us to this point, and to the many reviewers of the latest iteration of the PR (in particular @314eter, @c-cube, @clef-men, @damiendoligez, @dbuenzli, @gadmm, @Octachron and @wiktor).

The implementation uses an indirection to get a type-safe “empty” value to use in unused elements of the support array. Hopefully we can improve on that with a safe magical implementation in the short future – but I think that the performance is good enough already.

vdom 0.3: functional UI applications now with custom event handlers

Aurélien Saue announced

We are thrilled to announce the release of the new v0.3 release of vdom, previously named ocaml-vdom!

The library implements the functional Elm architecture. Combined with the power of OCaml, it makes the development of UI applications easy and reliable, and that is why we have been using it internally since 2016.

A highlight of this new version is the introduction of fully customizable event handlers, using Elm-style decoders. This enhancement simplifies the management of intricate browser events, such as retrieving drag-and-dropped files.

Read our blog post for more details about this new feature!

GitHub homepage: https://github.com/LexiFi/ocaml-vdom

Old CWN

If you happen to miss a CWN, you can send me a message and I’ll mail it to you, or go take a look at the archive or the RSS feed of the archives.

If you also wish to receive it every week by mail, you may subscribe to the caml-list.

2023-10-18

[Caml-list] APLAS 2023: Second Call for Participation

======================================================================
CALL FOR PARTICIPATION
Early registration deadline: 25 October 2023

21st Asian Symposium on Programming Languages and Systems (APLAS 2023)
Taipei, Taiwan, Sun 26 – Wed 29 November 2023

https://conf.researchr.org/home/aplas-2023
======================================================================

The 21st Asian Symposium on Programming Languages and
Systems (APLAS) aims to stimulate programming language
research by providing a forum for the presentation of
the latest results and the exchange of ideas in programming
languages and systems. APLAS is based in Asia but is an
international forum that serves the worldwide programming
languages community. This year's conference is co-located
with Agda Implementors' Meeting XXXVII.

APLAS 2023 will be held in Taipei, Taiwan from Monday 27th
to Wednesday 29th November 2023. Before the main conference,
the New Ideas and Emerging Results (NIER) workshop will be
held on Sunday 26th November 2023. There is also a student
research competition and an associated poster session.

======================================================================
# Participation
======================================================================

Registration information is available at the homepage:

https://conf.researchr.org/home/aplas-2023

Early registration deadline: 25 October 2023. Please
register soon!


======================================================================
# Keynote Speakers
======================================================================

* Hakjoo Oh, Korea University.
* Bow-Yaw Wang, Academia Sinica.

A third keynote speaker will be announced soon.

======================================================================
# Accepted Papers
======================================================================

* A Diamond Machine for Strong Evaluation.
Beniamino Accattoli (Inria & École Polytechnique), and
Pablo Barenbaum (National University of Quilmes (CONICET) &
University of Buenos Aires).

* Oracle Computability and Turing Reducibility in the
Calculus of Inductive Constructions.
Yannick Forster (Inria),
Dominik Kirst (Ben-Gurion University), and
Niklas Mück (Saarland University).

* m-CFA Exhibits Perfect Stack Precision.
Kimball Germane (Brigham Young University).

* Typed Non-determinism in Functional and Concurrent Calculi.
Bas van den Heuvel (University of Groningen),
Joseph W. N. Paulus (University of Groningen),
Daniele Nantes-Sobrinho (University of Brasília and
Imperial College London), and
Jorge Perez (University of Groningen)

* Argument Reduction of Constrained Horn Clauses Using
Equality Constraints.
Ryo Ikeda (The University of Tokyo),
Ryosuke Sato (The University of Tokyo), and
Naoki Kobayashi (The University of Tokyo).

* Transport via Partial Galois Connections and Equivalences.
Kevin Kappelmann (Technical University of Munich).

* Incorrectness Proofs for Object-Oriented Programs via
Subclass Reflection.
Wenhua Li (National University Singapore),
Quang Loc Le (University College London),
Yahui Song (National University of Singapore), and
Wei-Ngan Chin (National University of Singapore).

* Types and Semantics for Extensible Data Types.
Cas van der Rest (Delft University of Technology), and
Casper Bach Poulsen (Delft University of Technology).

* Experimenting with an Intrinsically-typed Probabilistic
Programming Language in Coq.
Ayumu Saito (Tokyo Institute of Technology),
Reynald Affeldt (National Institute of Advanced Industrial,
and Science and Technology (AIST)).

* TorchProbe: Fuzzing Dynamic Deep Learning Compilers.
Qidong Su (University of Toronto / Vector Institute),
Chuqin Geng (McGill University),
Gennady Pekhimenko (University of Toronto / Vector
Institute), and
Xujie Si (University of Toronto)

* What Types are Needed for Typing Dynamic Objects?
A Python-based Empirical Study.
Ke Sun (Peking University),
Sheng Chen (University of Louisiana at Lafayette),
Meng Wang (University of Bristol), and
Dan Hao(Peking University).

* Compilation Semantics for a Programming Language with
Versions.
Yudai Tanabe (Kyoto University),
Luthfan Anshar Lubis (Tokyo Institute of Technology),
Tomoyuki Aotani (Sanyo-Onoda City University), and
Hidehiko Masuhara (Tokyo Institute of Technology).

* A Fresh Look at Commutativity: Free Algebraic Structures
via Fresh Lists.
Sean Watters (University of Strathclyde),
Fredrik Nordvall Forsberg (University of Strathclyde), and
Clemens Kupke (University of Strathclyde).

* Proofs as Terms, Terms as Graphs.
Jui-Hsuan Wu (Institut Polytechnique de Paris).

* Towards a Framework for Developing Verified Assemblers
for the ELF Format.
Jinhua Wu (Shanghai Jiao Tong University),
Yuting Wang (Shanghai Jiao Tong University),
Meng Sun (Shanghai Jiao Tong University),
Xiangzhe Xu (Purdue University), and
Yichen Song (Shanghai Jiao Tong University).

======================================================================
# NIER Workshop
======================================================================

* λGT: A Functional Language with Graphs as First-Class Data
Kazunori Ueda and Jin Sano

* Environment-Friendly Monadic Equational Reasoning for OCaml
Jacques Garrigue, Reynald Affeldt and Takafumi Saikawa

* Counterfactual Explanations for Sequential Models through
Computational Complexity
Anthony Widjaja Lin

* Bottom-Up Construction of Sublist Trees
Shin-Cheng Mu

* A Neural-Network-Guided Approach to Program Verification
and Synthesis
Naoki Kobayashi

======================================================================
# POSTERS and STUDENT RESEARCH COMPETITION ENTRIES
======================================================================

* [Non-SRC] Encoding MELL Cut Elimination into a Hierarchical
Graph Rewriting Language
Kento Takyu, Kazunori Ueda

* [Non-SRC] Towards a Programming Paradigm Approach for
AI-Assisted Software Development
YungYu Zhuang, Wei-Hsin Yen, Yin-Jung Huang

* [SRC] Multiple Screen States for Programming with Small Screens
Jin Ishikawa

* [SRC] Relational Hoare Logic for Comparing Nondeterministic
Programs and Probabilistic Programs through a Categorical
Framework
Kazuki Matsuoka

* [SRC] Separate Compilation for Compositional Programming
via Extensible Records
Yaozhu Sun

* [SRC] Type-Safe Auto-Completion of Incomplete Polymorphic Programs
Yong Qi Foo

======================================================================
# ORGANIZERS
======================================================================

General Chair:
Shin-Cheng Mu, Academia Sinica, Taiwan

Program Chair:
Chung-Kil Hur, Seoul National University, Korea

Publicity Chair:
Ryosuke Sato, University of Tokyo, Japan

SRC and Posters Chair:
Hsiang-Shang 'Josh' Ko, Academia Sinica, Taiwan

Program Committee:

* Soham Chakraborty, TU Delft, Netherlands
* Yu-Fang Chen, Academia Sinica, Taiwan
* Ronghui Gu, Columbia University, USA
* Ichiro Hasuo, National Institute of Informatics, Japan
* Ralf Jung, ETH Zurich, Switzerland
* Ohad Kammar, University of Edinburgh, UK
* Jeehoon Kang, KAIST, Korea
* Jieung Kim, Inha University, Korea
* Robbert Krebbers, Radboud University Nijmegen, Netherlands
* Ori Lahav, Tel Aviv University, Israel
* Doug Lea, State University of New York at Oswego, USA
* Woosuk Lee, Hanyang University, Korea
* Hongjin Liang, Nanjing University, China
* Nuno P. Lopes, University of Lisbon, Portugal
* Chandrakana Nandi, Certora and UW, USA
* Liam O'Connor, The University of Edinburgh, UK
* Bruno C. d. S. Oliveira, The University of Hong Kong, Hong Kong
* Jihyeok Park, Korea University, Korea
* Clément Pit-Claudel, EPFL, Switzerland
* Matthieu Sozeau, Inria, France
* Kohei Suenaga, Kyoto University, Japan
* Tarmo Uustalu, Reykjavik University, Iceland
* John Wickerson, Imperial College London, UK
* Danfeng Zhang, Penn State University, USA

Posters Selection Committee

* Jacques Garrigue, Nagoya University, Japan
* Jeremy Gibbons, University of Oxford, UK
* Chih-Duo Hong, University of Oxford, UK
* Oleg Kiselyov, Tohoku University, Japan
* Akimasa Morihata, University of Tokyo, Japan
* Dominic Orchard, University of Kent, UK and
University of Cambridge, UK
* Taro Sekiyama, National Institute of Informatics, Japan
* Chung-chieh Shan, Indiana University, United States
* Youngju Song, MPI-SWS, Germany
* Tachio Terauchi, Waseda University, Japan
* Chuangjie Xu, Sonar Source, Germany

2023-10-02

[Caml-list] PADL'24: Last Call for Papers

==============================================================================
                        Call for Papers

  26th International Symposium on Practical Aspects of Declarative Languages
                          (PADL 2024)

              https://popl24.sigplan.org/home/PADL-2024

             London, United Kingdom, January 15-16, 2024

                   Co-located with ACM POPL 2024
==============================================================================


Conference Description
----------------------

Declarative languages comprise several well-established classes of
formalisms, namely, functional, logic, and constraint programming.
Such formalisms enjoy both sound theoretical bases and the
availability of attractive frameworks for application development.
Indeed, they have been already successfully applied to many different
real-world situations, ranging from database management to active
networks to software engineering to decision support systems.


New developments in theory and implementation fostered applications in
new areas. At the same time, applications of declarative languages to
novel and challenging problems raise many interesting research issues,
including designing for scalability, language extensions for
application deployment, and programming environments. Thus,
applications drive the progress in the theory and implementation of
declarative systems, and benefit from this progress as well.


PADL is a well-established forum for researchers and practitioners to
present original work emphasizing novel applications and
implementation techniques for all forms of declarative programming,
including functional and logic programming, database and constraint
programming, and theorem proving.


Topics of interest include, but are not limited to:


- Innovative applications of declarative languages
- Declarative domain-specific languages and applications
- Practical applications of theoretical results
- New language developments and their impact on applications
- Declarative languages and software engineering
- Evaluation of implementation techniques on practical applications
- Practical experiences and industrial applications
- Novel uses of declarative languages in the classroom
- Practical extensions such as constraint-based, probabilistic,
  and reactive languages


PADL 2024 especially welcomes new ideas and approaches related to
applications, design and implementation of declarative languages going
beyond the scope of the past PADL symposia, for example, advanced
database languages and contract languages, as well as verification and
theorem proving methods that rely on declarative languages.


Submissions
-----------

PADL 2024 welcomes three kinds of submission:

* Technical papers (max. 15 pages):
  Technical papers must describe original, previously unpublished
  research results.

* Application papers (max. 8 pages):
  Application papers are a mechanism to present important practical
  applications of declarative languages that occur in industry or in
  areas of research other than Computer Science. Application papers
  are expected to describe complex and/or real-world applications that
  rely on an innovative use of declarative languages. Application
  descriptions, engineering solutions and real-world experiences (both
  positive and negative) are solicited.

* Extended abstracts (max. 3 pages):
  Describing new ideas, a new perspective on already published work,
  or work-in-progress that is not yet ready for a full
  publication. Extended abstracts will be posted on the symposium
  website but will not be published in the formal proceedings.

All page limits exclude references. Submissions must be written in English
and formatted according to the standard Springer LNCS style, see
https://www.springer.com/gp/computer-science/lncs/conference-proceedings-guidelines

The review process of PADL 2024 is double-anonymous. In your submission, please, omit your names and institutions; refer to your prior work in the third person, just as you refer to prior work by others; do not include acknowledgements that might identify you.

Page numbers (and, if possible, line numbers) should appear on the
manuscript to help the reviewers in writing their reports. So, for
LaTeX, we recommend that authors use:

 \pagestyle{plain}
 \usepackage{lineno}
 \linenumbers

The conference proceedings of PADL 2024 will be published by
Springer-Verlag in the Lecture Notes in Computer Science series.
Work that already appeared in unpublished or informally published
workshop proceedings may be submitted but the authors should notify
the program chairs where it has previously appeared.

Papers should be submitted electronically at

https://padl2024.hotcrp.com 

Important Dates
---------------

Paper submission:    October 5, 2023 (AoE)
Notification:        November 9, 2023
Symposium:           January 15-16, 2024


Distinguished Papers
--------------------

The authors of a small number of distinguished papers will be invited
to submit a longer version for journal publication after the
symposium. For papers related to logic programming, that will be in
the journal Theory and Practice of Logic Programming (TPLP)
https://www.cambridge.org/core/journals/theory-and-practice-of-logic-programming,
and for papers related to functional programming, in Journal of
Functional Programming (JFP)
https://www.cambridge.org/core/journals/journal-of-functional-programming.
The extended journal submissions should be substantially (roughly 30%)
extended: explanations for which there was no space, illuminating examples
and proofs, additional definitions and theorems, further experimental
results, implementational details and feedback from
practical/engineering use, extended discussion of related work, and so
on. These submissions will then be subject to the usual peer review
process by the journal, although with the aim of a swifter review
process by reusing original reviews from PADL.


PADL 2024 PC Co-Chairs
----------------------
Martin Gebser, University of Klagenfurt, Austria
Ilya Sergey, National University of Singapore, Singapore


Programme Committee
-------------------
Alexandra Mendes          University of Porto & INESC TEC, Portugal
Annie Liu                 Stony Brook University, USA
Anton Trunov              Fuel Labs, UAE
Arnaud Spiwack            Tweag, France
Daniela Inclezan          Miami University, USA
Emilia Oikarinen          University of Helsinki, Finland
Enrico Pontelli           New Mexico State University, USA
Esra Erdem                Sabanci University, Turkey
Gopal Gupta               University of Texas at Dallas, USA
Jesper Cockx              Delft University of Technology, Netherlands
Jessica Zangari           University of Calabria, Italy
Johannes Wallner          Graz University of Technology, Austria
Leo White                 Jane Street, UK
Magnus Myreen             Chalmers University of Technology, Sweden
Manuel Carro              IMDEA Software Institute, Spain
Marcello  Balduccini      Saint Joseph's University, USA
Matthew Flatt             University of Utah, USA
Mukund Raghothaman        University of Southern California, USA
Patrick Bahr              University of Copenhagen, Denmark
Roland Yap                National University of Singapore, Singapore
Simon Fowler              University of Glasgow, UK
Stefania Costantini       University of L'Aquila, Italy
Tom Schrijvers            KU Leuven, Belgium
Tomi Janhunen             Tampere University, Finland
Weronika T. Adrian        University of Krakow, Poland
Youyou Cong               Tokyo Institute of Technology, Japan
Zeynep G. Saribatur       TU Wien, Austria