[Apologies for multiple copies]

=======================================================================
Call for Papers
UNIF 2024
The 38th International Workshop on Unification
Nancy, France, July 2, 2024
A satellite workshop of CADE/IJCAR, affiliated with IJCAR
https://lat.inf.tu-dresden.de/unif2024
=======================================================================

UNIF 2024 is the 38th event in a series of international meetings
devoted to unification theory and its applications. Unification is
concerned with the problem of making two given terms equal, either
syntactically or modulo an equational theory. It is a fundamental
process used in various areas of computer science, including automated
reasoning, term rewriting, logic programming, natural language
processing, program analysis, knowledge representation, types, etc.

The International Workshop on Unification (UNIF) is a forum for
researchers in unification theory and related fields to present recent
(even unfinished) work, and to discuss new ideas and trends. It is also
a good opportunity for students, young researchers and scientists working
in related areas to get an overview of the current state of the art in
unification theory.

Topics
------
A non-exhaustive list of topics of interest includes:

* syntactic and equational unification algorithms
* matching and constraint solving
* higher-order unification
* unification in modal, temporal, and description logics
* admissibility of inference rules
* narrowing
* disunification
* anti-unification
* complexity issues
* combination methods
* implementation techniques
* applications

Submission
----------

Short papers or extended abstracts, up to 5 pages in EasyChair style,
should be submitted electronically as PDF files through the EasyChair
submission site:

https://easychair.org/conferences/?conf=unif2024

Abstracts will be evaluated by the Program Committee regarding their
significance for the workshop. We allow submissions of work presented/
submitted in/to another conference.

Accepted abstracts will be presented at the workshop and included in
the informal proceedings of the workshop, available in electronic form
on the Web page of UNIF 2024. At least one of the authors should register
for the workshop.

Based on the number and quality of submissions we will decide whether to
organize a special journal issue.

Important Dates
---------------
* Paper submission: April 18, 2024 (AoE)
* Author notification: May 23, 2024 (AoE)
* Camera-ready version: June 7, 2024 (AoE)
* UNIF 2024: July 2, 2024

Invited Speakers
----------------

To be announced.

OCaml Weekly News

Previous Week Up Next Week

Hello

Here is the latest OCaml Weekly News, for the week of January 09 to 16, 2024.

Verifying an Effect-Based Cooperative Concurrency Scheduler in Iris, by Adrian Dapprich
OCaml Software Foundation: January 2024 update
Miou, a simple scheduler for OCaml 5
Grace 💅, fancy diagnostic library for compilers
Js_of_ocaml 5.5.2
First release of oma
Ocamlearlybird just got ability to inspect opaque/abstract values
Validate - A New Library for Data Validation
dune.3.12.1
Other OCaml News
Old CWN

Verifying an Effect-Based Cooperative Concurrency Scheduler in Iris, by Adrian Dapprich

Archive: https://discuss.ocaml.org/t/video-verifying-an-effect-based-cooperative-concurrency-scheduler-in-iris-by-adrian-dapprich/13825/1

Vincent Balat announced

Adrian Dapprich gave a talk at Tarides a few weeks ago, about Verifying an Effect-Based Cooperative Concurrency Scheduler in Iris. Here is a link to the video.

Abstract:

Lightweight asynchronous programming (using futures, goroutines or green threads) has been widely adopted to organize programs with many concurrent tasks, more than are traditionally feasible with thread-per-task models of concurrency. With the release of OCaml 5 and its support for effect handlers, the new concurrency library Eio was proposed which aims to replace previous monadic concurrency libraries for OCaml. In this work we verify the core fiber and promise abstractions of Eio and show their safety and effect safety using the Hazel program logic. Hazel is built on the Iris framework and allows reasoning about programs with effect handlers. We also adapt the existing proof of the verified CQS datastructure since Eio uses a customized version of CQS for its implementation of promises. We do not treat some features of Eio like cancellation, because it does not yield a verifiable specification, and resource control using switches, since it is a liveness property.

https://watch.ocaml.org/w/iQNqZzA8gVmd4RQaycAwx4

OCaml Software Foundation: January 2024 update

Archive: https://discuss.ocaml.org/t/ocaml-software-foundation-january-2024-update/13828/1

gasche announced

Happy new year!

This is an update update on recent works of the OCaml Software Foundation, covering our 2023 actions – the previous update was in January 2023.

The OCaml Software Foundation is a non-profit foundation (earlier thread) that receives funding from our industrial sponsors each year, and tries its best to spend it to support and strengthen the OCaml ecosystem and community.

The funding volume we receive each year is around 200K€. (For comparison: this is the yearly cost of one experienced full-time software engineer in many parts of the world.) We do not fund people full-time for long periods. Most actions receive from 3K€ to 20K€. The work to prepare and execute actions is mostly done by the (unpaid) Executive Committee. It is currently formed by Nicolás Ojeda Bär, Damien Doligez, Xavier Leroy, Kim Nguyễn, Virgile Prevosto and myself, with administrative personnel provided by INRIA and general assistance by Alan Schmitt.

Our current sponsors (thanks!) are ahrefs, Jane Street, Tezos, Bloomberg, Lexifi, SimCorp, MERCE and Tarides. (If your company would like to join as a sponsor, please get in touch. Unfortunately, we still cannot efficiently process small donations, so we are not calling for individual donations.)

Feel free to use this thread for questions/suggestions :-)

Recent actions

Teaching

We are funding an update and English translation (still in progress) of the French book Apprendre à Programmer avec OCaml, by Sylvain Conchon and Jean-Christophe Filliâtre, under the understanding that it will be released as open access content – online, at no cost. This is a good book that is suitable for use in classroom of first- or second-year university students of various level. (In comparison, OCaml from the Very Beginning and Real World OCaml are more aimed as self-study than use in classroom, and the Cornell CS3110 textbook is aimed at more advanced students with a strong background.)

For the second year in a row, we funded a Spanish summer school on functional programming in OCaml, organized in Saragossa by Ricardo Rodriguez and Roberto Blanco. This is an occasion for students to discover OCaml and functional programming, and the organizers also run a one-day mini-workshop for the students and anyone interested (including online), the Day of the Caml.

Outreach

We are funding the recurring OCaml Meetup in Paris; this year we are also funding a new meetup in Toulouse, a city in the south-west region of France known for duck cuisine, white beans, and strong aerospace industry. If you are interested in organizing an OCaml meetup in your city, and some light funding would help, please get in touch!

We got in touch with the organizers of the ICFP 2023 conference to ensure that colocated workshops (which include the OCaml Workshop) can be attended online at low or no cost. The ICFP organizers accepted to (semi-officially) make virtual attendance free, so we tried to encourage broad participation to the OCaml Workshop. We also supported the OCaml Workshop by funding the expenses of some of the program committee members to attend, when they do not have an employer in academia or industry that can easily reimburse their trip.

We are supporting the work of Alan Schmitt on the Caml Weekly Newsletter (CWN).

Kim Nguyễn ran the OCaml User Survey 2023 for the OCaml Foundation – we have not posted the survey results yet.

We invited Sudha Parimala to propose more actions oriented towards diversity and inclusion. A first step is the inclusion of demographic questions in the 2023 survey, to get a better picture of the current composition of the OCaml community.

Ecosystem

Infrastructure

As in previous years, we are funding Kate Deplaix to work on “release readiness” of the OCaml ecosystem: when a new OCaml release is being prepared, Kate checks the compatibility of all opam packages with the upcoming release and gets in touch with maintainers to contribute or request support for the new version. The OCaml 5 transition has been a lot of work for Kate on this front – mostly not due to the Multicore runtime changes, but the removal of various long-deprecated functions of our C and OCaml APIs.

For almost as long as we can remember, Kate Deplaix has also been the most active maintainer of the opam-repository – the person who provides feedback when there is a packaging issue in a new PR to the opam-repository, to interpret CI failures, recommend best packaging practices, etc. (Kate’s work on this topic was funded by OCamllabs then Tarides, not the OCaml Foundation.) Kate decided recently to move on to other things – notably, contributions to opam. (There was a call for volunteers on Discuss around that time.) This was a bit of a scare for us as the good health of the public opam-repository is central to the functioning of the current OCaml free software ecosystem. We were already providing financial support (in the form of research funding) to Marcello Seri, the second most-active contributor, and renewed our support. We also got in touch with other opam-repository contributors, and started funding the work of Haochen Xie.
Tools

We got in touch with frequent Dune contributors to offer financial support for their contributions. Ali Caglayan was supported in this way in 2023.

We are supporting some of the work of Jonah Beckford on Windows support of OCaml, as well as his work on mentoring OCaml students in the Seattle area. If you want to learn about Jonah’s work, consider watching his April 2023 talk at the Houston Functional Programmers meetup.

Simmo Saan spontaneously took up maintenance of ocamlearlybird, the bytecode debugger frontend that integrates with visual studio code – we had previously funded ocamlearlybird maintenance, but its Wen moved to a demanding startup and was not available to work on ocamlearlybird anymore. We are funding the time of Simmo Saan, who accomplished a lot in a short amount of time, notably the integration of the ocamlearlybird plugin in the main OCaml plugin for vscode.

We will be funding one year of post-doc by Takafumi Saikawa at Nagoya University, to continue his work with Jacques Garrigue on the refactoring of the OCaml type-checker. The type-checker codebase suffers from technical debt, and the effort led by Jacques in the last few year has been precious in making it easier to understand, improve and extend for other developers.
Libraries
We funded work by Alan Hu to improve the OCaml LLVM bindings, to support newer LLVM releases and make them compatible with OCaml 5. Alan announced this work on Discuss.

We support the contributions of Daniel Bünzli to the OCaml ecosystem. Daniel used this support to fund the development of
- cmarkit, a new Markdown parser and renderer for OCaml, and ocamlmark a tool to use Markdown to write OCaml documentation comments,
- WebGPU support in brr, his browser interaction toolkit
- support for Unicode 15.0 and 15.1 in his Unicode libraries
- zipc, a pure-OCaml ZIP archiver.
We continued providing partial support for the work of Antonio Monteiro on Melange. In 2023, Antonio announced Melange 1.0.

We are supporting the work of Petter Urkedal on the Caqti library, the main database connection library in the OCaml community. Caqti 2 was released in 2023.

We will be supporting the time of Nathan Rebours to contribute to the maintenance of ppxlib.

Miou, a simple scheduler for OCaml 5

Archive: https://discuss.ocaml.org/t/ann-miou-a-simple-scheduler-for-ocaml-5/12963/13

Calascibetta Romain announced

I’m delighted to announce the beta2 release of Miou. This summarises the feedback we’ve received and specifies the API that this library should offer in terms of scheduling.

As a reminder, Miou is intended to be simple and designed for developing services and integrating into a unikernel. We were talking about implementing a library such as happy-eyeballs with Miou, but we have now made available a library that implements an HTTP client and/or server (http/1.1, h2 as well as alpn support via ocaml-tls).

This has enabled us to find bugs typical of a transition between OCaml 4 and OCaml 5, in particular illegal parallel access to data on mirage-crypto (although we would like to observe the implications in terms of performance of our fix).

We will of course continue to listen and experiment with Miou in order to develop this library in a way that suits us and our users. The documentation has been updated accordingly and is now available here.

Grace 💅, fancy diagnostic library for compilers

Archive: https://discuss.ocaml.org/t/ann-grace-fancy-diagnostic-library-for-compilers/13834/1

Alistair O’Brien announced

It is my pleasure to announce the initial release of Grace, a cutting-edge OCaml library 🐪 that includes a series of interfaces for building, reporting, and rendering beautiful compiler diagnostics.

To get started, simply run:

opam update  opam install grace

Key features

📐 Inline and multi-line error messages with associated priorities
📂 Multi-file errors
⚙️ Configurable rendering (styling and character set)
🌈 Coloured messages for ANSI terminals
💪 100% OCaml

The project is still in its early phase with many additional features planned:

📚 Unicode support
⚡️ LSP integration with linol
👀 Accessibility features such improved colour options and narratable renderers

I invite the community to play with Grace, exploring its capabilities and limitations. Your insights will play a crucial role in shaping the future of this library :)

Js_of_ocaml 5.5.2

Archive: https://discuss.ocaml.org/t/ann-js-of-ocaml-5-5-2/13581/2

Hhugo announced

Js_of_ocaml 5.6 was released recently with many fixes related to its javascript parser/printer/minifier

First release of oma

Archive: https://discuss.ocaml.org/t/ann-first-release-of-oma/13845/1

François Pottier announced

Hello,

It is my pleasure to announce the first release of Oma. This library offers an implementation of the order maintenance data structure described in this paper.

  opam update    opam install oma

Here is its documentation.

Happy hacking!

Ocamlearlybird just got ability to inspect opaque/abstract values

Archive: https://discuss.ocaml.org/t/ann-ocamlearlybird-just-got-ability-to-inspect-opaque-abstract-values/13852/1

文宇祥 announced

I’m pleased to announce the release of ocamlearlybird.1.3.0. It should soon be able available in opam.

A big feature just landed. You can inspect opaque/abstract values since version 1.3.0.

see https://github.com/hackwaly/ocamlearlybird/pull/53

Validate - A New Library for Data Validation

Archive: https://discuss.ocaml.org/t/ann-validate-a-new-library-for-data-validation/13861/1

Mateusz Ledwoń announced

Hello!

I’m excited to announce the preview release of a new library called validate! This library aims to make the process of validating records, lists, or individual values more streamlined and efficient.

validate operates through a PPX deriver that automatically generates validators using annotations. It comes with an array of helper validation functions for different data types, making it versatile and easy to integrate into your projects.

Example Usage:

Imagine you have a record type with various fields that need validation. With validate, you can easily annotate these fields and the library will handle the rest. For example:

type my_record = {    min : string; [@min_length 2]    email : string; [@email]    uuid : string; [@uuid]    url : string; [@url] [@max_length 200]    numeric_list : int list; [@list_min_length 2] [@less_than 10]    other_record: other; [@dive]  } [@@deriving validate]

This will automatically create a validate_my_record function, applying the specified validations to each field.

Installation: You can install validate using OPAM:

Copy code

  opam install validate

I encourage you to try it out, and your feedback and contributions are invaluable at this stage.

For more details, please visit GitHub repository and check out the documentation.

dune.3.12.1

Archive: https://discuss.ocaml.org/t/ann-dune-3-12-1/13536/2

Etienne Millon announced

We just released version 3.12.2 with 2 bugfixes:

Fix version check in runtest_alias for cram stanza (#9454, @emillon)
Fix stack overflow when a (run) action can not be parsed. (#9530, fixes #9529, @gridbugs)

Other OCaml News

From the ocaml.org blog

Here are links from many OCaml blogs aggregated at the ocaml.org blog.

Meet odoc, OCaml’s Documentation Generator

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.

Alan Schmitt

Calls for participation

2024-01-31

[Caml-list] CGO24 - Early-bird Deadline Registration

2024-01-17

[Caml-list] UNIF 2024 Call for Papers

2024-01-16

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