======================================================================== CALL FOR PAPERS FSCD 2027 International Conference on Formal Structures for Computation and Deduction Radboud University Nijmegen, The Netherlands 23-26 August 2027 https://fscd-conference.org/2027 ======================================================================== FSCD (https://fscd-conference.org/) covers all aspects of formal structures for computation and deduction, from theoretical foundations to applications. Building on two communities, RTA (Rewriting Techniques and Applications) and TLCA (Typed Lambda Calculi and Applications), FSCD embraces their core topics and broadens their scope to closely related areas in logic, models of computation, semantics and verification in new challenging areas. ------------------------------------------------------------------------ IMPORTANT DATES ------------------------------------------------------------------------ All deadlines are midnight anywhere-on-earth (AoE); late submissions will not be considered. • Abstract: 19 April 2027 • Submission: 26 April 2027 • Author Response: 8-12 June 2027 • Notification: 28 June 2027 • Final Version: 10 July 2027 ------------------------------------------------------------------------ LIST OF TOPICS ------------------------------------------------------------------------ The suggested, but not exclusive, list of topics for submission is: 1. Calculi - Rewriting systems (string, term, higher-order, nominal, graph, conditional, modulo, infinitary, etc.) - Lambda calculus - Logics (first-order, higher-order, equational, modal, linear, classical, constructive, etc.) - Proof theory (natural deduction, sequent calculus, proof nets, etc.) - Type theory and logical frameworks - Homotopy type theory - Process algebras (synchronous, asynchronous, static and dynamic semantics with and without time, etc.) - Quantum calculi 2. Methods in Computation and Deduction - Type systems (polymorphism, dependent, recursive, intersection, session, etc.) - Induction, coinduction - Matching, unification, completion, orderings - Strategies (normalisation, completeness, etc.) - Tree automata - Model building and model checking - Proof search and theorem proving - Constraint solving and decision procedures 3. Semantics - Operational semantics and abstract machines - Game semantics and applications - Domain theory and categorical models - Quantitative models (timing, probabilities, etc.) - Quantum computation and emerging models of computation 4. Algorithmic Analysis and Transformations of Formal Systems - Type inference and type checking - Abstract interpretation - Complexity analysis and implicit computational complexity - Checking termination, confluence, derivational complexity and related properties - Symbolic computation 5. Formal Systems for Modelling and Verification - Machine learning algorithms - Neuro-symbolic systems - Certification - Security - Blockchain - Databases - Planning 6. Tools and Applications - Programming and proof environments - Verification tools - Proof assistants and interactive theorem provers - Applications in industry - Applications of formal systems in other sciences - Applications of formal systems in education ------------------------------------------------------------------------ PUBLICATION ------------------------------------------------------------------------ The proceedings will be published as an electronic volume in the Leibniz International Proceedings in Informatics (LIPIcs) of Schloss Dagstuhl. All LIPIcs proceedings are open access. ------------------------------------------------------------------------ SPECIAL ISSUE ------------------------------------------------------------------------ There will be a special issue of Logical Methods in Computer Science of selected papers. More details will be provided later. ------------------------------------------------------------------------ SUBMISSION GUIDELINES ------------------------------------------------------------------------ The submission site is: https://easychair.org/conferences/?conf=fscd2027 Submissions must be formatted using the LIPIcs style files and submitted via EasyChair. Submissions can be made in two categories: * Regular research papers are limited to 15 pages, excluding references and appendices. They must present original research which is unpublished and not submitted elsewhere. * System descriptions are limited to 15 pages, excluding references. Shorter papers are welcome and will be given equal consideration. A system description must present new software tools, or significantly new versions of such tools, in which FSCD topics play an important role. An archive of the code with instructions on how to install and run the tool must be submitted. In addition, a webpage where the system can be experimented with should be provided. Submissions must be unpublished and not submitted for publication elsewhere. They will be judged on relevance, significance, originality, correctness, and readability. Reviewers may consider material provided in appendices, but submissions must be self-contained within the page limit. If software or data is relevant to a paper, a link that provides access to the software/data must be provided to enable reproduction of results. One author of each accepted paper is expected to register and present the work in person at the conference. In case this is not possible, online presentation will be arranged, but in-person registration will still be required. ------------------------------------------------------------------------ BEST PAPER AWARD BY JUNIOR RESEARCHERS ------------------------------------------------------------------------ The programme committee will select a paper in which at least one author is a junior researcher, i.e. either a student or someone whose PhD award date is less than three years from the first day of the meeting. When submitting the paper, other authors should declare to the PC Chair that at least 50% of the contribution is made by the junior researcher(s). ------------------------------------------------------------------------ COMMITTEES ------------------------------------------------------------------------ Program Committee Chairs - Mariangiola Dezani-Ciancaglini (University of Torino, Italy) - Daniele Nantes-Sobrinho (University of Brasilia, Brazil) Program Committee - Sandra Alves (UPorto) - Takahito Aoto (Niigata University) - Mauricio Ayala-Rincon (Universidade de Brasilia) - Franz Baader (TU Dresden) - Luis Caires (Universidade NOVA de Lisboa) - Malgorzata Biernacka (University of Wroclaw) - Alejandro Diaz-Caro (Inria / LORIA & UNQ) - Andrej Dudenhefner (Dortmund University) - Santiago Escobar (Universitat Politecnica de Valencia) - Claudia Faggian (CNRS - Paris 7) - Maribel Fernandez (King's College London) - Yannick Forster (INRIA) - Simon Gay (University of Glasgow) - Samir Genaim (Universidad Complutense de Madrid) - Silvia Ghilezan (Novi Sad University) - Ekaterina Komendantskaya (Heriot-Watt University) - Dexter Kozen (Cornell University) - Temur Kutsia (RISC, Johannes Kepler University Linz) - Marina Lenisa (University of Udine) - Giulio Manzonetto (IRIF, Paris Cite University) - Sonia Marin (University of Birmingham) - Catherine Meadows (Naval Research Laboratory) - Jose Meseguer (University of Illinois Urbana-Champaign) - Aart Middeldorp (University of Innsbruck) - Samuel Mimram (Ecole Polytechnique) - Paliath Narendran (University at Albany--SUNY) - Naoki Nishida (Nagoya University) - Valeria de Paiva (Topos Institute, California) - Jorge Perez (University of Groningen) - Frank Pfenning (Carnegie Mellon University) - Christophe Ringeissen (INRIA) - Alwen Tiu (The Australian National University) - Stephanie Weirich (University of Pennsylvania) Conference Chair - Herman Geuvers (Radboud University Nijmegen, The Netherlands) Workshop Chair - Cynthia Kop (Radboud University Nijmegen, The Netherlands) ------------------------------------------------------------------------ INVITED SPEAKERS ------------------------------------------------------------------------ TBD ------------------------------------------------------------------------ VENUE AND DATES ------------------------------------------------------------------------ Radboud University Nijmegen, The Netherlands 23-26 August 2027 ------------------------------------------------------------------------ SPONSORS ------------------------------------------------------------------------ TBD ------------------------------------------------------------------------ CONTACT ------------------------------------------------------------------------ All questions about submissions should be emailed to: Daniele Nantes-Sobrinho (dnantes 'at' unb.br) Mariangiola Dezani-Ciancaglini (dezani 'at' di.unito.it) ========================================================================
OCaml Weekly News
Hello
Here is the latest OCaml Weekly News, for the week of September 29 to October 06, 2026.
Table of Contents
- tinybox: 150 classic games (Pong to Quake) and Apps, in OCaml, and more
- IX, a full OS (kernel, toolchain, vcs, …) in OCaml
- Michel Mauny, 1959-2026
- dream-html 4.0.0
- hegel-ocaml 0.25.0 - concurrent stateful property-based testing
- Tutorial on GADTs
- OCaml Compiler Implemented in C++: It's Not Just Faster—It Also Increases Trust
- Conf.funcp.org is a scam OCaml conference
- Vaast 0.0.0 + Design discussion
- a2a SDK in OCaml
- Old CWN
tinybox: 150 classic games (Pong to Quake) and Apps, in OCaml, and more
Yoann Padioleau announced
Hi,
I made something. Well Claude made something, my first vibe coded project :slight_smile: An ode to code, 150 classic video games (from Pong to Quake), 50 classic apps (from VisiCalc and TurboPascal to Office and Chrome), all playable online and you can also admire their tiny OCaml code. repo: https://github.com/aryx/ocaml-elm-playground
the tinybox web app to play: https://aryx.github.io/ocaml-elm-playground/tinybox.html
IX, a full OS (kernel, toolchain, vcs, …) in OCaml
Yoann Padioleau announced
Hi,
It is my pleasure to announce IX, a full operating system written in OCaml (by Claude Code). It is a continuation of two of my past projects, principia softwarica and XiX.
Repo: https://github.com/aryx/IX
website: https://aryx.github.io/IX/
You can even explore the codebase with a nice visualizer, codemapv2 (itself a rewrite, using Claude, of two of my past projects, codemap and codegraph done while at Facebook): https://aryx.github.io/IX/codemap.html Some literate books explaining in detail the code will arrive soon. Enjoy!
Michel Mauny, 1959-2026
gasche announced
Dear all,
It is with great sadness that we (the OCaml Software Foundation) are sharing the news of the death of Michel Mauny, a long-time member of the OCaml community. Michel passed away on September 17th 2026 (more information, in French).
During his career as INRIA research scientist, professor at ENSTA and CEO of Nomadic Labs, and among his many contributions, Michel:
- co-authored in 1985 the paper that started Caml: "The Categorical Abstract Machine", Cousineau, Curien, Mauny (PDF) ;
- actively contributed in the late 80s to the "Heavy Caml" implementation that predated Caml Light and OCaml ( see https://ocaml.org/history for more details ) ;
- introduced stream parsers with Daniel de Rauglaudre (1992 tech report), designed and co-maintained the camlp4 preprocessor ;
- wrote with Guy Cousineau the first book in English about OCaml, "The functional approach to programming" (1998) ;
- taught (O)Caml in French universities and engineering schools throughout his career (Paris 7, Polytechnique, ENSTA) ;
- advised several PhD students, including several who remained active in the OCaml community: Grégoire Henry, Çağdaş Bozman, Benoît Vaugon and Pierrick Couderc ;
- created in 2001 the Caml Consortium, an earlier structure for industrial users to participate in and fund the development of OCaml at INRIA ;
- created in 2018 the OCaml Foundation, with the more ambitious goals of collecting more funds to also support the broader OCaml software ecosystem. Michel had to leave the OCaml Foundation when he moved from INRIA to Nomadic Labs, and we try our best to follow his vision.
This solemn moment is also an occasion to reflect on the rich history of our OCaml ecosystem, which grows by a collection of individual contributions. As we mark Michel’s passing, we celebrate and thank him, as well as the many individuals who dedicate their time and effort, often over decades, to building our programming commons.
dream-html 4.0.0
Yawar Amin announced
Hi, dream-html 4.0.0 has been released to opam: https://ocaml.org/p/dream-html/4.0.0
Repo: https://github.com/yawaramin/dream-html API docs: https://yawaramin.github.io/dream-html/dream-html/Dream_html/index.html
Dream-html is a library for generating HTML, closely integrated with Dream. It can be used as an alternative to Dream’s built-in Embedded ML templating language and comes with all current htmx attributes defined out of the box.
In this release, I made a few breaking changes (hence major version bump):
- Raise exceptions on path parameter parse errors: instead of responding with 400 Bad Request. This allows you to hook in your own custom response by catching the parse exception.
- Remove unused form decoder error keys: specifically
error_expected_int32anderror_expected_int64which are already covered byerror_expected_int. - Finally, revert to the previous style of HTML generation, breaking lines at the start of each attribute instead of pretty-printing the HTML with indentation. This is done for performance reasons.
Fixes:
- Router matching on encoded values, eg
/accounts/%F0%9F%91%8D/versions/1is now able to extract the second segment,👍.
New additions:
- Invoker API attributes
- Some more SVG elements
Finally, raised the minimum supported OCaml version to 5.3.0 because of ppxlib.
Enjoy!
hegel-ocaml 0.25.0 - concurrent stateful property-based testing
Ethan Chou announced
Hello, we excited to announce hegel-ocaml 0.25.0!
Since our last announcement of hegel-ocaml 0.14.1, we've added concurrent stateful property-based testing and nondeterminism handling to Hegel. Stateful property based testing sequences actions (which we call rules) that mutate the state of some model and the system under test. The concurrent part comes from running rules concurrently. Hegel spins up some number of workers and distributes some number of rules to each worker. Rules within a worker run sequentially, but rules in different workers may run concurrently. Of course, this introduces nondeterminism since the workers can run in any order or suspend. To handle this, Hegel repeatedly replays failures and outputs the number of times the failure was reproduced. Nondeterminism handling can also be turned off, so any nondeterministic failure produces a flaky test error instead. Of course, running Hegel inside of Antithesis will give reproducible failures.
For an example of concurrent stateful testing, see the docs.
The unique feature of Hegel concurrent stateful tests is the ability to pass in different concurrency capabilities. Workers can be on threads, domains, or anything of the Concurrency.t type. We have included a thread capability and domains capability for your convenience. Hegel defaults to using threads.
With the hegel_jane_async sublibrary, Jane Street ecosystem users can also run sequential stateful tests whose rules are async (returning unit Deferred.t).
For OxCaml users, hegel-ocaml is fully compatible with OxCaml 5.2.0-minus39. With the hegel_jane_concurrent sublibrary, OxCaml users can also pass in concurrency capabilities from the Concurrent library. and run concurrent async stateful tests with hegel_jane_async.
Happy testing and contributing!
Tutorial on GADTs
Continuing this thread, Raphaël Proust announced
I've written a supplement to the tutorial:
https://raphael-proust.gitlab.io/code/gadt-what-about-phantom-types.html
It compares GADTs and Phantom Types. It includes a (compulsory?) mention of Tyxml in discussion of Phantom Types. If anyone has other good examples to share I might add them.
OCaml Compiler Implemented in C++: It's Not Just Faster—It Also Increases Trust
Michael Bacarella announced
You're absolutely right to be skeptical of your compiler binaries. In this post, we'll explore how a comprehensive C++ reimplementation unlocks DDC verification for OCaml — while delivering meaningful compile-time improvements. 🚀
—
Wait! Don't leave yet! The rest of this was typed character by character by a human.
We had some fun here recently talking about an unrelated project, the OCaml runtime ported to Rust, and this led to an interesting side-channel discussion that surfaced a paper on Debootstrapping without Archeology by Nathanaëlle Courant, Julien Lepiller and Gabriel Scherer. I somehow had never come across this before!
Background brief on trusting trust: once upon a time, UNIX god Ken Thompson trolled the world during an acceptance speech by asking "wouldn't it be hilarious if your beloved compiler authors had introduced a backdoor years (decades) ago that was still lurking today???" (paraphrased). The crux of the matter was that, to compile a C compiler which is implemented in C, you need an existing C compiler binary and that's an opportunity to introduce malware that wakes up when it recognizes it's compiling a target program (like login).
Ever since then, the infosec community has been… curious… about trusting trust and they breathed a huge sigh of relief when David A. Wheeler proposed diverse double compilation (DDC) as a mitigation. So, has anyone done this for our favorite language?
Yes! In the Debootstrapping OCaml paper, the authors describe writing an OCaml interpreter in MiniML (an OCaml subset) and a compiler for MiniML in Scheme to do DDC, which proved that OCaml 4.07.1 has no trusting trust backdoors when compiling itself. But notice this part in their paper:
If we assume unlimited work resources, tailored debootstrapping is a trivial problem: just port your programming-language implementation to another language that has already been debootstrapped (for example C). But this is a massive effort that may never happen in practice – especially as you have to first convince your language implementors to work in a different programming language.
Tee hee.
I present this independent OCaml compiler implemented in C++. It runs a OOMs faster than the MiniML/Scheme debootstrapper, solves DDC for OCaml 5.5.1 release (and 5.6+trunk), produces identical byte outputs to the OCaml compiler, and it even runs faster than the official OCaml compiler(!)
NOTE for quick skimmers: this project does not make your OCaml programs faster. It may only let you compile OCaml programs faster.
Regarding byte-identical outputs. There's a few documented minor divergences that could be closed if there's interest. The divergences do not preclude DDC and they're minor enough that I am claiming byte identical.
Most importantly: because we have done DDC, we can conclude the OCaml 5.5.1 (and 5.6+trunk) bootstrap has no back doors when compiling the compiler. Furthermore, because we do produce byte identical outputs as upstream, arguably no back door is lurking outside of the source-available views.[1]
Regrettably, not only is there no backdoor in the OCaml compiler, there isn't even an easter egg. Sad! I would have at least snuck in something like mb4c4rell4_waz_here, but that's probably why the good people behind OCaml have commit bits and I don't.
How to run DDC yourself
Clone the repo git clone https://github.com/mbacarella/cxx-ocaml and follow the instructions in cxx/DDC.md.
Install an opam switch that uses the C++-based OCaml compiler
Do this to get a switch whose ocamlc and ocamlopt are the C++ version.
opam switch create cxx-5.5 --empty opam pin add -n ocaml-variants.5.5.1 'git+https://github.com/mbacarella/cxx-ocaml#cxx-5.5' opam pin add -n ocaml-option-cxx.1 'git+https://github.com/mbacarella/cxx-ocaml#cxx-5.5' opam install ocaml-option-cxx ocaml-variants opam switch set-invariant --packages=ocaml-variants,ocaml-option-cxx
To check that you're actually running the C++ version, do ocamlc -cxx-version. The stock compiler stays available in the switch as ocaml*.stock.
Requirements: clang++ 18 or newer, cmake, ninja, and libzstd's dev files.
Don't @ me that this is all a big hoax because you're missing some dependencies. We have all seen how that goes.
Next steps
Minimize the extra dependencies needed above, like swapping clang for gcc to match OCaml upstream.
I've only tested this on x86-64 on Linux, so ARM64 is an obvious next addition. Also probably should add support for flambda.
There's still some low hanging performance-fruit wins that don't involve doing anything too obscene[2] to go after.
I'm happy to hear your feedback! We can chat here or on the OCaml Discord's #ai channel.
Let me know what you'd like to see!
Benchmarks
Take these with a grain of salt. Benchmarks are easy to embarass yourself with. That said.
My benchmark host was a Desktop Ryzen 9 7950X with 128GB of RAM running Linux.
I'd prepare an opam switch with each compiler and all project dependencies first.
The benchmark itself is a full build of awso, an AWS library that has coverage for all of 300+ AWS services, including some very huge auto-generated modules with ppx.
It builds byte code, native and assembles a gigantic awso-cli that links every aws library. I timed dune build and took the best of 3.
I think this is a good real world test because it contains about 100,000 build artifacts and it was a major quality of life issue to both do full rebuilds every time I tinkered with something. opam-ci certainly didn't appreciate how huge it was either.
dune selected up to 32 cores on my host.
Results
- ocaml 5.5.1: 4998.41s user 1016.62s system 1904% cpu 5:15.91 total
- c++ocaml 5.5.1: 3281.87s user 990.02s system 1984% cpu 3:35.30 total
As we can see, both the CPU time and wall clock time are lower in the C++ version. In terms of wall time we are 1.47x faster.
Every build artifact is bitwise identical to upstream: .cmi, .cmo, .cmx, .o, .cma, .cmxa. So are executables built in the same switch (in the C++ switch the stock compiler is ocamlopt.stock and the C++ version is renamed over ocamlopt). The one difference is the .cmt/.cmti files, which are used by editor tooling. They decode to the same data but stock OCaml's marshalling has a form of structural sharing we didn't completely reproduce the layout of.[3]
Note there's more than just the ocaml compiler itself running a build. A ton of time is spent in the gcc toolchain (like as). The improvement in individual artifacts is more substantial than the wall clock time suggests, but it's also a lot more work to describe. So I'll leave that for later if anyone is interested.
AI disclosure
I obviously didn't implement an OCaml compiler in C++ myself. I used Claude Code. This wasn't easy for Claude either: it has been working on this project for 4 months now, though progress sped up between the releases of Opus 4.8, 5.0 and 5.5, with some guest appearances by Fable.
This is not an April fool's
Don't confuse this with Stephen Dolan's troll, which compiled OCaml into C++ template metaprograms. Game respects game though.
Conf.funcp.org is a scam OCaml conference
Cuihtlauac Alvarado announced
This site:
Presents as an OCaml/Haskell/FP conference. However:
- The event is not listed on the venue's official schedule: https://www.javitscenter.com/calendar
- The funcp.org domain was registered two weeks ago, yet the oldest blog posts are dated from April: https://rdap.org/domain/funcp.org
- The domain has no email routing — the contact addresses cannot receive mail: https://mxtoolbox.com/emailhealth/funcp.org/
- Registration routes payment off-site to a third-party platform (gomry.com), with a $149+ ticket.
- Listed speakers or organisers don't seem to have any track record in our community
- Talk's topics don't stand scrutiny
- Claims to be a second edition, but I can't find a prior edition
If you registered, I suggest cancelling and getting your money back.
This has been reported to the OCaml and Haskell security teams, the Javits Center, Google Safe Browsing, Cloudflare, dev.events (which lists the conference), and Gomry (the payment platform).
Thanks to @adrien, @mtelvers and @edwin, who helped disclose this.
Vaast 0.0.0 + Design discussion
fantazio announced
Hi all,
This is a bit of mixed post.
I am excited to announce the 1st prototype of Vaast ! Vaast is a library to handle multiple versions of the Typedtree at once. It is meant as a replacement for the current compiler-version-dependent techniques (be it preprocessing or branching).
Similarly to ppxlib for the Parsetree, it provides a single representation of the Typedtree. Unlike ppxlib, it does not select a compiler version's representation but provides a form of super-representation which embeds the Typedtree from OCaml 4.14 to 5.5 at once. It does so via a dedicated type encoding which explicitly and precisely identifies the differences in-between versions.Vaast's Typedtree representation is a shallow replacement for OCaml's Typedtree, making it cheap to use and easy to integrate incrementally in existing code.
More details on its design are available on my blog: https://fantazio.eu/articles/designing_vaast.html
This leads us to the second part of this post: discussing the design. The prototype is usable as a replacement for the compiler's Typedtree (and I experimented it on the dead_code_analyzer). Overall its design resembles the Typedtree but limits the breakages in user-code when updating to a more recent OCaml version.
Here is an example of code in odoc, relying on cppo to handle the different versions of the Typedtree:
#if defined OXCAML
| Tpat_alias (_, id, loc, _uid, _, _, _) -> (
#elif OCAML_VERSION >= (5, 4, 0)
| Tpat_alias (_, id, loc, _uid, _ty) -> (
#elif OCAML_VERSION >= (5, 2, 0)
| Tpat_alias (_, id, loc, _uid) -> (
#else
| Tpat_alias (_, id, loc) -> (