diff --git a/analysis/index.html~ b/analysis/index.html~
deleted file mode 100644
index 7c7f8d1a..00000000
--- a/analysis/index.html~
+++ /dev/null
@@ -1,272 +0,0 @@
-<?xml version="1.0" encoding="utf-8"?>
-<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
-"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
-<html xmlns="http://www.w3.org/1999/xhtml" lang="en" xml:lang="en">
-<head>
-<!-- 2024-03-31 Sun 20:29 -->
-<meta http-equiv="Content-Type" content="text/html;charset=utf-8" />
-<meta name="viewport" content="width=device-width, initial-scale=1" />
-<title>Mathematical Components compliant Analysis Library</title>
-<meta name="generator" content="Org mode" />
-<meta name="author" content="Reynald Affeldt" />
-<style type="text/css">
- <!--/*--><![CDATA[/*><!--*/
-  .title  { text-align: center;
-             margin-bottom: .2em; }
-  .subtitle { text-align: center;
-              font-size: medium;
-              font-weight: bold;
-              margin-top:0; }
-  .todo   { font-family: monospace; color: red; }
-  .done   { font-family: monospace; color: green; }
-  .priority { font-family: monospace; color: orange; }
-  .tag    { background-color: #eee; font-family: monospace;
-            padding: 2px; font-size: 80%; font-weight: normal; }
-  .timestamp { color: #bebebe; }
-  .timestamp-kwd { color: #5f9ea0; }
-  .org-right  { margin-left: auto; margin-right: 0px;  text-align: right; }
-  .org-left   { margin-left: 0px;  margin-right: auto; text-align: left; }
-  .org-center { margin-left: auto; margin-right: auto; text-align: center; }
-  .underline { text-decoration: underline; }
-  #postamble p, #preamble p { font-size: 90%; margin: .2em; }
-  p.verse { margin-left: 3%; }
-  pre {
-    border: 1px solid #ccc;
-    box-shadow: 3px 3px 3px #eee;
-    padding: 8pt;
-    font-family: monospace;
-    overflow: auto;
-    margin: 1.2em;
-  }
-  pre.src {
-    position: relative;
-    overflow: visible;
-    padding-top: 1.2em;
-  }
-  pre.src:before {
-    display: none;
-    position: absolute;
-    background-color: white;
-    top: -10px;
-    right: 10px;
-    padding: 3px;
-    border: 1px solid black;
-  }
-  pre.src:hover:before { display: inline;}
-  /* Languages per Org manual */
-  pre.src-asymptote:before { content: 'Asymptote'; }
-  pre.src-awk:before { content: 'Awk'; }
-  pre.src-C:before { content: 'C'; }
-  /* pre.src-C++ doesn't work in CSS */
-  pre.src-clojure:before { content: 'Clojure'; }
-  pre.src-css:before { content: 'CSS'; }
-  pre.src-D:before { content: 'D'; }
-  pre.src-ditaa:before { content: 'ditaa'; }
-  pre.src-dot:before { content: 'Graphviz'; }
-  pre.src-calc:before { content: 'Emacs Calc'; }
-  pre.src-emacs-lisp:before { content: 'Emacs Lisp'; }
-  pre.src-fortran:before { content: 'Fortran'; }
-  pre.src-gnuplot:before { content: 'gnuplot'; }
-  pre.src-haskell:before { content: 'Haskell'; }
-  pre.src-hledger:before { content: 'hledger'; }
-  pre.src-java:before { content: 'Java'; }
-  pre.src-js:before { content: 'Javascript'; }
-  pre.src-latex:before { content: 'LaTeX'; }
-  pre.src-ledger:before { content: 'Ledger'; }
-  pre.src-lisp:before { content: 'Lisp'; }
-  pre.src-lilypond:before { content: 'Lilypond'; }
-  pre.src-lua:before { content: 'Lua'; }
-  pre.src-matlab:before { content: 'MATLAB'; }
-  pre.src-mscgen:before { content: 'Mscgen'; }
-  pre.src-ocaml:before { content: 'Objective Caml'; }
-  pre.src-octave:before { content: 'Octave'; }
-  pre.src-org:before { content: 'Org mode'; }
-  pre.src-oz:before { content: 'OZ'; }
-  pre.src-plantuml:before { content: 'Plantuml'; }
-  pre.src-processing:before { content: 'Processing.js'; }
-  pre.src-python:before { content: 'Python'; }
-  pre.src-R:before { content: 'R'; }
-  pre.src-ruby:before { content: 'Ruby'; }
-  pre.src-sass:before { content: 'Sass'; }
-  pre.src-scheme:before { content: 'Scheme'; }
-  pre.src-screen:before { content: 'Gnu Screen'; }
-  pre.src-sed:before { content: 'Sed'; }
-  pre.src-sh:before { content: 'shell'; }
-  pre.src-sql:before { content: 'SQL'; }
-  pre.src-sqlite:before { content: 'SQLite'; }
-  /* additional languages in org.el's org-babel-load-languages alist */
-  pre.src-forth:before { content: 'Forth'; }
-  pre.src-io:before { content: 'IO'; }
-  pre.src-J:before { content: 'J'; }
-  pre.src-makefile:before { content: 'Makefile'; }
-  pre.src-maxima:before { content: 'Maxima'; }
-  pre.src-perl:before { content: 'Perl'; }
-  pre.src-picolisp:before { content: 'Pico Lisp'; }
-  pre.src-scala:before { content: 'Scala'; }
-  pre.src-shell:before { content: 'Shell Script'; }
-  pre.src-ebnf2ps:before { content: 'ebfn2ps'; }
-  /* additional language identifiers per "defun org-babel-execute"
-       in ob-*.el */
-  pre.src-cpp:before  { content: 'C++'; }
-  pre.src-abc:before  { content: 'ABC'; }
-  pre.src-coq:before  { content: 'Coq'; }
-  pre.src-groovy:before  { content: 'Groovy'; }
-  /* additional language identifiers from org-babel-shell-names in
-     ob-shell.el: ob-shell is the only babel language using a lambda to put
-     the execution function name together. */
-  pre.src-bash:before  { content: 'bash'; }
-  pre.src-csh:before  { content: 'csh'; }
-  pre.src-ash:before  { content: 'ash'; }
-  pre.src-dash:before  { content: 'dash'; }
-  pre.src-ksh:before  { content: 'ksh'; }
-  pre.src-mksh:before  { content: 'mksh'; }
-  pre.src-posh:before  { content: 'posh'; }
-  /* Additional Emacs modes also supported by the LaTeX listings package */
-  pre.src-ada:before { content: 'Ada'; }
-  pre.src-asm:before { content: 'Assembler'; }
-  pre.src-caml:before { content: 'Caml'; }
-  pre.src-delphi:before { content: 'Delphi'; }
-  pre.src-html:before { content: 'HTML'; }
-  pre.src-idl:before { content: 'IDL'; }
-  pre.src-mercury:before { content: 'Mercury'; }
-  pre.src-metapost:before { content: 'MetaPost'; }
-  pre.src-modula-2:before { content: 'Modula-2'; }
-  pre.src-pascal:before { content: 'Pascal'; }
-  pre.src-ps:before { content: 'PostScript'; }
-  pre.src-prolog:before { content: 'Prolog'; }
-  pre.src-simula:before { content: 'Simula'; }
-  pre.src-tcl:before { content: 'tcl'; }
-  pre.src-tex:before { content: 'TeX'; }
-  pre.src-plain-tex:before { content: 'Plain TeX'; }
-  pre.src-verilog:before { content: 'Verilog'; }
-  pre.src-vhdl:before { content: 'VHDL'; }
-  pre.src-xml:before { content: 'XML'; }
-  pre.src-nxml:before { content: 'XML'; }
-  /* add a generic configuration mode; LaTeX export needs an additional
-     (add-to-list 'org-latex-listings-langs '(conf " ")) in .emacs */
-  pre.src-conf:before { content: 'Configuration File'; }
-
-  table { border-collapse:collapse; }
-  caption.t-above { caption-side: top; }
-  caption.t-bottom { caption-side: bottom; }
-  td, th { vertical-align:top;  }
-  th.org-right  { text-align: center;  }
-  th.org-left   { text-align: center;   }
-  th.org-center { text-align: center; }
-  td.org-right  { text-align: right;  }
-  td.org-left   { text-align: left;   }
-  td.org-center { text-align: center; }
-  dt { font-weight: bold; }
-  .footpara { display: inline; }
-  .footdef  { margin-bottom: 1em; }
-  .figure { padding: 1em; }
-  .figure p { text-align: center; }
-  .equation-container {
-    display: table;
-    text-align: center;
-    width: 100%;
-  }
-  .equation {
-    vertical-align: middle;
-  }
-  .equation-label {
-    display: table-cell;
-    text-align: right;
-    vertical-align: middle;
-  }
-  .inlinetask {
-    padding: 10px;
-    border: 2px solid gray;
-    margin: 10px;
-    background: #ffffcc;
-  }
-  #org-div-home-and-up
-   { text-align: right; font-size: 70%; white-space: nowrap; }
-  textarea { overflow-x: auto; }
-  .linenr { font-size: smaller }
-  .code-highlighted { background-color: #ffff00; }
-  .org-info-js_info-navigation { border-style: none; }
-  #org-info-js_console-label
-    { font-size: 10px; font-weight: bold; white-space: nowrap; }
-  .org-info-js_search-highlight
-    { background-color: #ffff00; color: #000000; font-weight: bold; }
-  .org-svg { width: 90%; }
-  /*]]>*/-->
-</style>
-<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
-<style type="text/css"> body {font-family: Arial, Helvetica; margin-left: 5em; font-size: large;} </style>
-<style type="text/css"> h1 {margin-left: 0em; padding: 0px; text-align: center} </style>
-<style type="text/css"> h2 {margin-left: 0em; padding: 0px; color: #580909} </style>
-<style type="text/css"> h3 {margin-left: 1em; padding: 0px; color: #C05001;} </style>
-<style type="text/css"> body { max-width: 1100px; width: 100% - 30px; margin-left: 30px; }</style>
-<script type="text/javascript">
-/*
-@licstart  The following is the entire license notice for the
-JavaScript code in this tag.
-
-Copyright (C) 2012-2020 Free Software Foundation, Inc.
-
-The JavaScript code in this tag is free software: you can
-redistribute it and/or modify it under the terms of the GNU
-General Public License (GNU GPL) as published by the Free Software
-Foundation, either version 3 of the License, or (at your option)
-any later version.  The code is distributed WITHOUT ANY WARRANTY;
-without even the implied warranty of MERCHANTABILITY or FITNESS
-FOR A PARTICULAR PURPOSE.  See the GNU GPL for more details.
-
-As additional permission under GNU GPL version 3 section 7, you
-may distribute non-source (e.g., minimized or compacted) forms of
-that code without the copy of the GNU GPL normally required by
-section 4, provided you include this license notice and a URL
-through which recipients can access the Corresponding Source.
-
-
-@licend  The above is the entire license notice
-for the JavaScript code in this tag.
-*/
-<!--/*--><![CDATA[/*><!--*/
- function CodeHighlightOn(elem, id)
- {
-   var target = document.getElementById(id);
-   if(null != target) {
-     elem.cacheClassElem = elem.className;
-     elem.cacheClassTarget = target.className;
-     target.className = "code-highlighted";
-     elem.className   = "code-highlighted";
-   }
- }
- function CodeHighlightOff(elem, id)
- {
-   var target = document.getElementById(id);
-   if(elem.cacheClassElem)
-     elem.className = elem.cacheClassElem;
-   if(elem.cacheClassTarget)
-     target.className = elem.cacheClassTarget;
- }
-/*]]>*///-->
-</script>
-</head>
-<body>
-<div id="content">
-<h1 class="title">Mathematical Components compliant Analysis Library</h1>
-<p>
-The purpose of this page is to list up the automatically generated HTML documentation of
-<a href="https://github.com/math-comp/analysis">MathComp-Analysis</a>.
-</p>
-
-<div id="outline-container-org6a5e638" class="outline-2">
-<h2 id="org6a5e638">Documentation of MathComp-Analysis</h2>
-<div class="outline-text-2" id="text-org6a5e638">
-<ul class="org-ul">
-<li><a href="htmldoc_1_1_0/index.html">1.1.0</a>, <a href="htmldoc_1_0_0/index.html">1.0.0</a></li>
-<li><a href="htmldoc_0_7_0/index.html">0.7.0</a></li>
-<li><a href="htmldoc_0_6_7/index.html">0.6.7</a>, <a href="htmldoc_0_6_6/index.html">0.6.6</a>, <a href="htmldoc_0_6_5/index.html">0.6.5</a>, <a href="htmldoc_0_6_4/index.html">0.6.4</a>, <a href="htmldoc_0_6_3/index.html">0.6.3</a>, <a href="htmldoc_0_6_2/index.html">0.6.2</a>, <a href="htmldoc_0_6_1/index.html">0.6.1</a>, (<a href="htmldoc_master_alectryon">master</a> <span class="timestamp-wrapper"><span class="timestamp">[2023-02-12 Sun] </span></span> using <a href="https://github.com/math-comp/analysis/pull/458">Alectryon</a> (tentative)) <a href="htmldoc_0_6_0/index.html">0.6.0</a></li>
-<li><a href="htmldoc_0_5_3/index.html">0.5.3</a>, <a href="htmldoc_0_5_2/index.html">0.5.2</a>, <a href="htmldoc_0_5_1/index.html">0.5.1</a>, <a href="htmldoc_0_5_0/index.html">0.5.0</a></li>
-<li><a href="htmldoc_0_4_0/index.html">0.4.0</a></li>
-<li><a href="htmldoc_0_3_13/index.html">0.3.13</a></li>
-</ul>
-</div>
-</div>
-</div>
-</body>
-</html>
diff --git a/papers.html b/papers.html
index 02c9d6ed..3e3e0bfa 100644
--- a/papers.html
+++ b/papers.html
@@ -3,11 +3,11 @@
 "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
 <html xmlns="http://www.w3.org/1999/xhtml" lang="en" xml:lang="en">
 <head>
-<!-- 2024-10-10 Thu 08:31 -->
+<!-- 2024-10-25 Fri 14:49 -->
 <meta http-equiv="Content-Type" content="text/html;charset=utf-8" />
 <meta name="viewport" content="width=device-width, initial-scale=1" />
 <title>Mathematical Components: Research Papers</title>
-<meta name="author" content="Yves Bertot" />
+<meta name="author" content="Reynald Affeldt" />
 <meta name="generator" content="Org Mode" />
 <style>
   #content { max-width: 60em; margin: auto; }
@@ -207,10 +207,10 @@ <h1 class="title">Mathematical Components: Research Papers</h1>
 <h2>Table of Contents</h2>
 <div id="text-table-of-contents" role="doc-toc">
 <ul>
-<li><a href="#org0ce73fd">Mathematics</a></li>
-<li><a href="#org5b5b679">Programming and Algorithms</a></li>
-<li><a href="#org3f4f4cd">Other Applications</a></li>
-<li><a href="#org2cd229c">Tooling</a></li>
+<li><a href="#orge8a15c3">Mathematics</a></li>
+<li><a href="#orge4b6d2e">Programming and Algorithms</a></li>
+<li><a href="#org86926ee">Other Applications</a></li>
+<li><a href="#org62dac1f">Tooling</a></li>
 </ul>
 </div>
 </div>
@@ -240,9 +240,9 @@ <h2>Table of Contents</h2>
 Please, send <a href="mailto:mathcomp-dev@inria.fr?subject=MathComp%20related%20paper">us</a> a message or <a href="https://github.com/math-comp/math-comp.github.io">issue/PR on github</a>.
 </p>
 
-<div id="outline-container-org0ce73fd" class="outline-2">
-<h2 id="org0ce73fd">Mathematics</h2>
-<div class="outline-text-2" id="text-org0ce73fd">
+<div id="outline-container-orge8a15c3" class="outline-2">
+<h2 id="orge8a15c3">Mathematics</h2>
+<div class="outline-text-2" id="text-orge8a15c3">
 <ul class="org-ul">
 <li>Reynald Affeldt, Zachary Stone.
 <span class="underline">A Comprehensive Overview of the Lebesgue Differentiation Theorem in Coq</span>.
@@ -355,9 +355,9 @@ <h2 id="org0ce73fd">Mathematics</h2>
 </ul>
 </div>
 
-<div id="outline-container-org53cc570" class="outline-3">
-<h3 id="org53cc570">Graph Theory</h3>
-<div class="outline-text-3" id="text-org53cc570">
+<div id="outline-container-org384e522" class="outline-3">
+<h3 id="org384e522">Graph Theory</h3>
+<div class="outline-text-3" id="text-org384e522">
 <ul class="org-ul">
 <li>Christian Doczkal.
 <span class="underline">A Variant of Wagner’s Theorem Based on Combinatorial Hypermaps</span>.
@@ -379,9 +379,9 @@ <h3 id="org53cc570">Graph Theory</h3>
 </div>
 </div>
 
-<div id="outline-container-org0fb6df2" class="outline-3">
-<h3 id="org0fb6df2">Robotics</h3>
-<div class="outline-text-3" id="text-org0fb6df2">
+<div id="outline-container-org1695762" class="outline-3">
+<h3 id="org1695762">Robotics</h3>
+<div class="outline-text-3" id="text-org1695762">
 <ul class="org-ul">
 <li>Yves Bertot,
 <span class="underline">Safe Smooth Paths Between Straight Line Obstacles</span>.
@@ -397,10 +397,13 @@ <h3 id="org0fb6df2">Robotics</h3>
 </div>
 </div>
 
-<div id="outline-container-org5b5b679" class="outline-2">
-<h2 id="org5b5b679">Programming and Algorithms</h2>
-<div class="outline-text-2" id="text-org5b5b679">
+<div id="outline-container-orge4b6d2e" class="outline-2">
+<h2 id="orge4b6d2e">Programming and Algorithms</h2>
+<div class="outline-text-2" id="text-orge4b6d2e">
 <ul class="org-ul">
+<li>Cyril Cohen, Kazuhiko Sakaguchi.
+<span class="underline">A bargain for mergesorts (functional pearl) &#x2013; How to prove your mergesort correct and stable, almost for free</span>.
+arXiv 2024. <a href="https://arxiv.org/pdf/2403.08173">pdf</a></li>
 <li>Ana de Almeida Borges, Mireia González Bedmar, Juan Conejero Rodríguez, Eduardo Hermo Reyes, Joaquim Casals Buñuel, Joost J. Joosten.
 <span class="underline">UTC time, formally verified</span>.
 CPP 2024. <a href="https://arxiv.org/pdf/2209.14227.pdf">pdf</a></li>
@@ -450,9 +453,9 @@ <h2 id="org5b5b679">Programming and Algorithms</h2>
 </ul>
 </div>
 
-<div id="outline-container-orga90da71" class="outline-3">
-<h3 id="orga90da71">Concurrency</h3>
-<div class="outline-text-3" id="text-orga90da71">
+<div id="outline-container-org962e36d" class="outline-3">
+<h3 id="org962e36d">Concurrency</h3>
+<div class="outline-text-3" id="text-org962e36d">
 <ul class="org-ul">
 <li>Mohit Tekriwal, Avi Tachna-Fram, Jean-Baptiste Jeannin, Manos Kapritsos, Dimitra Panagou.
 <span class="underline">Formally verified asymptotic consensus in robust networks</span>.
@@ -498,9 +501,9 @@ <h3 id="orga90da71">Concurrency</h3>
 </div>
 </div>
 
-<div id="outline-container-orga531a4f" class="outline-3">
-<h3 id="orga531a4f">Information Flow</h3>
-<div class="outline-text-3" id="text-orga531a4f">
+<div id="outline-container-org4e00f44" class="outline-3">
+<h3 id="org4e00f44">Information Flow</h3>
+<div class="outline-text-3" id="text-org4e00f44">
 <ul class="org-ul">
 <li>Aleksandar Nanevski, Anindya Banerjee, Deepak Garg.
 <span class="underline">Dependent Type Theory for Verification of Information Flow and Access Control Policies</span>.
@@ -515,9 +518,9 @@ <h3 id="orga531a4f">Information Flow</h3>
 </div>
 </div>
 
-<div id="outline-container-orgb3af9aa" class="outline-3">
-<h3 id="orgb3af9aa">Probabilistic Reasoning</h3>
-<div class="outline-text-3" id="text-orgb3af9aa">
+<div id="outline-container-orge4396bf" class="outline-3">
+<h3 id="orge4396bf">Probabilistic Reasoning</h3>
+<div class="outline-text-3" id="text-orge4396bf">
 <ul class="org-ul">
 <li>Reynald Affeldt, Clark Barrett, Alessandro Bruni, Ieva Daukantas, Harun Khan, Takafumi Saikawa, Carsten Schürmann.
 <span class="underline">Robust Mean Estimation by All Means (short paper)</span>.
@@ -549,9 +552,9 @@ <h3 id="orgb3af9aa">Probabilistic Reasoning</h3>
 </div>
 </div>
 
-<div id="outline-container-org3f61b26" class="outline-3">
-<h3 id="org3f61b26">Quantum Computing</h3>
-<div class="outline-text-3" id="text-org3f61b26">
+<div id="outline-container-orge4a59df" class="outline-3">
+<h3 id="orge4a59df">Quantum Computing</h3>
+<div class="outline-text-3" id="text-orge4a59df">
 <ul class="org-ul">
 <li>Jacques Garrigue and Takafumi Saikawa.
 <span class="underline">Typed compositional quantum computation with lenses</span>.
@@ -564,9 +567,9 @@ <h3 id="org3f61b26">Quantum Computing</h3>
 </div>
 </div>
 
-<div id="outline-container-org3f4f4cd" class="outline-2">
-<h2 id="org3f4f4cd">Other Applications</h2>
-<div class="outline-text-2" id="text-org3f4f4cd">
+<div id="outline-container-org86926ee" class="outline-2">
+<h2 id="org86926ee">Other Applications</h2>
+<div class="outline-text-2" id="text-org86926ee">
 <ul class="org-ul">
 <li>Pierre-Léo Bégay, Pierre Crégut, Jean-François Monin.
 <span class="underline">Developing and certifying Datalog optimizations in Coq/MathComp</span>. CPP 2021. <a href="https://hal.archives-ouvertes.fr/hal-03065304v1/document">pdf</a></li>
@@ -580,9 +583,9 @@ <h2 id="org3f4f4cd">Other Applications</h2>
 </ul>
 </div>
 
-<div id="outline-container-org099a457" class="outline-3">
-<h3 id="org099a457">Logic, Types, and Verification</h3>
-<div class="outline-text-3" id="text-org099a457">
+<div id="outline-container-org4bad64f" class="outline-3">
+<h3 id="org4bad64f">Logic, Types, and Verification</h3>
+<div class="outline-text-3" id="text-org4bad64f">
 <ul class="org-ul">
 <li>Jan Bessai, Jakob Rehof, Boris Düdder.
 <span class="underline">Fast Veriﬁed BCD Subtyping</span>.
@@ -619,9 +622,9 @@ <h3 id="org099a457">Logic, Types, and Verification</h3>
 </div>
 </div>
 
-<div id="outline-container-org8eeee48" class="outline-3">
-<h3 id="org8eeee48">Information Theory</h3>
-<div class="outline-text-3" id="text-org8eeee48">
+<div id="outline-container-orga2611c6" class="outline-3">
+<h3 id="orga2611c6">Information Theory</h3>
+<div class="outline-text-3" id="text-orga2611c6">
 <ul class="org-ul">
 <li>Joshua M. Cohen, Qinshi Wang, Andrew W. Appel.
 <span class="underline">Verified Erasure Correction in Coq with MathComp and VST</span>.
@@ -650,13 +653,16 @@ <h3 id="org8eeee48">Information Theory</h3>
 </div>
 </div>
 
-<div id="outline-container-org2cd229c" class="outline-2">
-<h2 id="org2cd229c">Tooling</h2>
-<div class="outline-text-2" id="text-org2cd229c">
+<div id="outline-container-org62dac1f" class="outline-2">
+<h2 id="org62dac1f">Tooling</h2>
+<div class="outline-text-2" id="text-org62dac1f">
 <ul class="org-ul">
 <li>Cyril Cohen, Enzo Crance, Assia Mahboubi.
 <span class="underline">Trocq: Proof Transfer for Free, With or Without Univalence</span>.
 ESOP 2024. <a href="https://arxiv.org/pdf/2310.14022">pdf</a></li>
+<li>Xavier Allamigeon, Quentin Canu, Cyril Cohen, Kazuhiko Sakaguchi, Pierre-Yves Strub.
+<span class="underline">Design patterns of hierarchies for order structures</span>.
+HAL 2023. <a href="https://inria.hal.science/hal-04008820/document">pdf</a></li>
 <li>Valentin Blot, Denis Cousineau, Enzo Crance, Louise Dubois de Prisque, Chantal Keller, Assia Mahboubi, Pierre Vial.
 <span class="underline">Compositional Pre-processing for Automated Reasoning in Dependent Type Theory</span>.
 CPP 2023. <a href="https://arxiv.org/pdf/2204.02643.pdf">pdf</a></li>
@@ -699,9 +705,9 @@ <h2 id="org2cd229c">Tooling</h2>
 </ul>
 </div>
 
-<div id="outline-container-orga0574c9" class="outline-3">
-<h3 id="orga0574c9">Machine Learning</h3>
-<div class="outline-text-3" id="text-orga0574c9">
+<div id="outline-container-org6defe0e" class="outline-3">
+<h3 id="org6defe0e">Machine Learning</h3>
+<div class="outline-text-3" id="text-org6defe0e">
 <ul class="org-ul">
 <li>Reynald Affeldt, Alessandro Bruni, Ekaterina Komendantskaya, Natalia Ślusarz, Kathrin Stark.
 <span class="underline">Taming Differentiable Logics with Coq Formalisation</span>.
diff --git a/papers.org b/papers.org
index f507101b..743a8d35 100644
--- a/papers.org
+++ b/papers.org
@@ -179,6 +179,9 @@ This is a memo to serve in the event we change the sectioning
 
 * Programming and Algorithms
 
+- Cyril Cohen, Kazuhiko Sakaguchi.
+  _A bargain for mergesorts (functional pearl) -- How to prove your mergesort correct and stable, almost for free_.
+  arXiv 2024. [[https://arxiv.org/pdf/2403.08173][pdf]]
 - Ana de Almeida Borges, Mireia González Bedmar, Juan Conejero Rodríguez, Eduardo Hermo Reyes, Joaquim Casals Buñuel, Joost J. Joosten.
   _UTC time, formally verified_.
   CPP 2024. [[https://arxiv.org/pdf/2209.14227.pdf][pdf]]
@@ -395,6 +398,9 @@ This is a memo to serve in the event we change the sectioning
 - Cyril Cohen, Enzo Crance, Assia Mahboubi.
   _Trocq: Proof Transfer for Free, With or Without Univalence_.
   ESOP 2024. [[https://arxiv.org/pdf/2310.14022][pdf]]
+- Xavier Allamigeon, Quentin Canu, Cyril Cohen, Kazuhiko Sakaguchi, Pierre-Yves Strub.
+  _Design patterns of hierarchies for order structures_.
+  HAL 2023. [[https://inria.hal.science/hal-04008820/document][pdf]]
 - Valentin Blot, Denis Cousineau, Enzo Crance, Louise Dubois de Prisque, Chantal Keller, Assia Mahboubi, Pierre Vial.
   _Compositional Pre-processing for Automated Reasoning in Dependent Type Theory_.
   CPP 2023. [[https://arxiv.org/pdf/2204.02643.pdf][pdf]]
