- Haskell-Cafe - Haskell.org

AI for Math Summer Fellowship -- Copilots for Isabelle (Sheffield / Copenhagen / London): application deadline April 10
by Andrei Popescu 21 Mar '26

21 Mar '26

Dear Colleagues, We are pleased to advertise an AI for Math Summer Fellowship opportunity on the project "Copilots for Isabelle: Learning Logical Structure for a Better Proving Experience". The general call and application details (including an application link) can be found here: https://docs.google.com/document/d/1tXlT2A2NyLi_N-Fn1Q5zwG6J0b8Cwhzj/edit Please note that the application deadline is April 10, and the internship will run for 10 weeks, from June 15 to August 21, 2026. In this project, the selected fellow will work with researchers at the University of Sheffield, University of Copenhagen, and King’s College London on developing AI-based copilots for the Isabelle proof assistant. The aim is to leverage the rich structure of interactive proofs to build intelligent tools that assist with proof development, documentation, and automation. The fellowship offers the opportunity to work on topics such as: -- generating polished proofs from informal or partial drafts, -- automatically producing documentation for Isabelle/ML code, -- adapting and tuning LLMs for proof tasks. The position is open to undergraduate, master’s and PhD students, and can be carried out in Sheffield, Copenhagen, or London (with support for travel if needed). Please see the attached project description for further details. Best wishes, Andrei, Dmitriy and Mohammad

1 0

GHC 9.12.4-rc1 is now available
by Zubin Duggal 18 Mar '26

18 Mar '26

The GHC developers are very pleased to announce the availability of the release candidate for GHC 9.12.4. Binary distributions, source distributions, and documentation are available at [downloads.haskell.org][] and via [GHCup](https://www.haskell.org/ghcup/). GHC 9.12.4 is a bug-fix release fixing many issues of a variety of severities and scopes, including: * Fixed a critical code generation regression where sub-word division produced incorrect results (#26711, #26668), similar to the bug fixed in 9.12.2 * Numerous fixes for register allocation bugs, preventing data corruption when spilling and reloading registers (#26411, #26526, #26537, #26542, #26550) * Fixes for several compiler crashes, including issues with CSE (#25468), SetLevels (#26681), implicit parameters (#26451), and the type-class specialiser (#26682) * Fixed cast worker/wrapper incorrectly firing on INLINE functions (#26903) * Fixed LLVM backend miscompilation of bit manipulation operations (#20645, #26065, #26109) * Fixed associated type family and data family instance changes not triggering recompilation (#26183, #26705) * Fixed negative type literals causing the compiler to hang (#26861) * Improvements to determinism of compiler output (#26846, #26858) * Fixes for eventlog shutdown deadlocks (#26573) and lost wakeups in the RTS (#26324) * Fixed split sections support on Windows (#26696, #26494) and the LLVM backend (#26770) * Fixes for the bytecode compiler, PPC native code generator, and Wasm backend * The runtime linker now supports COMMON symbols (#6107) * Improved backtrace support: backtraces for `error` exceptions are now evaluated at throw time * `NamedDefaults` now correctly requires the class to be standard or have an in-scope default declaration, and handles poly-kinded classes (#25775, #25778, #25882) * ... and many more A full accounting of these fixes can be found in the [release notes][]. As always, GHC's release status, including planned future releases, can be found on the GHC Wiki [status][]. This release candidate will have a two-week testing period. If all goes well the final release will be available the week of 26 March 2026. GHC development is sponsored by: * [Juspay](https://juspay.com/) * [QBayLogic](https://qbaylogic.com/) * [Channable](https://www.channable.com/) * [Haskell Foundation](https://haskell.foundation/) * [Serokell](https://serokell.io/) * [Well-Typed](https://well-typed.com/) * [Tweag](https://www.tweag.io/) * [Dotcom-Monitor](https://www.dotcom-monitor.com/) * [LoadView](https://www.loadview-testing.com/) * [Web Hosting Buddy](https://webhostingbuddy.com/) * [Find My Electric](https://www.findmyelectric.com/) * [Standard Chartered](https://www.sc.com) * [UpCloud](https://upcloud.com) * [Mercury](https://mercury.com) We would like to thank these sponsors and other anonymous contributors whose on-going financial and in-kind support has facilitated GHC maintenance and release management over the years. Finally, this release would not have been possible without the hundreds of open-source contributors whose work comprise this release. As always, do give this release a try and open a [ticket][] if you see anything amiss. [release notes]: https://gitlab.haskell.org/ghc/ghc/-/blob/ghc-9.12/docs/users_guide/9.12.4-… [status]: https://gitlab.haskell.org/ghc/ghc/-/wikis/GHC-status [downloads.haskell.org] https://downloads.haskell.org/ghc/9.12.4-rc1 [ticket]: https://gitlab.haskell.org/ghc/ghc/-/issues/new

2 4

Midlands Graduate School, 13-17 April 2026, Nottingham
by Graham Hutton (staff) 17 Mar '26

17 Mar '26

Dear all, There are just a few days left now to register for this years Midlands Graduate School (MGS) in Nottingham. Eight fantastic courses on type theory, category theory, lambda calculus and more. 13-17 April 2026, Nottingham, UK. Registration closes Sunday 22nd March. Best wishes, Graham ========================================================== MIDLANDS GRADUATE SCHOOL 2026 13-17 April 2026, Nottingham, UK https://tinyurl.com/MGS-2026 ========================================================== BACKGROUND The Midlands Graduate School (MGS) in the Foundations of Computing Science provides a yearly programme of courses on the mathematical foundations of computing, and recently celebrated its 25th year. The MGS is primarily aimed at PhD students in their first or second year, but is open to everyone, and has increasingly seen participation from industry. We welcome participants from all over the world! COURSES Eight courses will be given. Participants usually take around four courses, depending on their interests. Invited course: - Implement your POPL paper (using Haskell) Stephanie Weirich (Pennsylvania) Introductory courses: - Type Theory using Agda Thorsten Altenkirch (Nottingham) - Category Theory Sergey Goncharov (Birmingham) - Lambda Calculus and Combinatory Algebra Sam Speight (Birmingham) Advanced courses: - Effects and Call-By-Push-Value Paul Blain Levy (Birmingham) - Synthetic Homotopy Theory Axel Ljungström (Nottingham) - Categorical Algebra and Logic Sean Moss (Birmingham) - Inductive and Coinductive Reasoning with Isabelle/HOL Andrei Popescu (Sheffield) REGISTRATION Student participants: £350 (or £600 with accommodation) Industry participants: £800 (or £1050 with accommodation) The registration fee includes all lecture courses and example classes, lunch and coffee breaks, and the conference dinner. The 'with accommodation' options include five nights at Rutland Hall with shared bathroom facilities. Registration closes Sunday 22nd March. Spaces are limited, so please register early to secure your place. SPONSORSHIP We offer a range of sponsorship opportunities for industry (bronze, silver, gold and platinum), each with specific benefits. Please see the website for further details. LOCAL ORGANISERS For any queries, please contact the local organisers: Ulrik Buchholtz <ulrik.buchholtz(a)nottingham.ac.uk> Dan Marsden <dan.marsden(a)nottingham.ac.uk> ========================================================== -- Professor Graham Hutton School of Computer Science University of Nottingham, UK http://people.cs.nott.ac.uk/pszgmh This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored where permitted by law.

1 0

Hackage down?
by Ivan Perez 13 Mar '26

13 Mar '26

Hi cafe, I just received this when trying to access hackage: Error 503 Backend unavailable, connection timeout Backend unavailable, connection timeout Error 54113 Details: cache-pao-kpao1770051-PAO 1773366957 2060396358 ------------------------------ Varnish cache server Is this known? Thanks, Ivan

3 2

Second CfP: Festschrift and Workshop in Honor of David Basin (Deadline: 21st May 2026)
by Achim D. Brucker 10 Mar '26

10 Mar '26

Dear Fellow Researchers! Our dear colleague and friend David Basin is turning 65 in December 2026 and this has to be celebrated! We therefore organize a Festschrift and a Fest to celebrate his birthday and his extensive research contributions! The Fest/celebration itself will be held as a one-day event on the 15th of January 2027 at ETH Zürich. We have already checked that David is available. You do not have to keep it a secret - on the contrary, it is great if you share this message with anybody who might like to contribute! We hereby cordially invite you to contribute an article to the Festschrift and present it at the Fest. We welcome contributions in all areas close to David's research and interests, including but not limited to security, privacy, formal methods, logic, automated reasoning, model checking, theorem proving, software engineering, bridge, juggling, biking and more. The articles will be lightly reviewed by the Festschrift committee, and the proceedings will be **published by Springer Heidelberg in the LNCS series**. David will of course love to receive a research article from you, but also short personal articles that celebrate the history and friendship with David will be very much appreciated. We would like to set a deadline for submissions at the 21st of May 2026 via our submission site <https://easychair.org/conferences/?conf=feschi2027>. Articles should be formatted in Springer’s LNCS style and not exceed 5 pages for personal articles and 16 pages for scientific articles. If you have a work that you would like to contribute that does not fit into this page limit, it might be possible, but please reach out to us first. There will be no participation fee for the Fest and coffee breaks, lunch, and dinner will be included. Travel and accommodation costs are at the expense of the participants. We are happy to provide hotel suggestions for Zürich. Submission Information: * Format: 16 pages in LNCS format, templates available at: <https://www.springer.com/gp/computer-science/lncs/conference-proceedings-gu…> * Submission: <https://easychair.org/conferences/?conf=feschi2027> * Website (under construction) with updates and further information: <https://feschi2027.github.io/> * Timeline: * Submission: 21 May 2026 * Notification: end of June 2026 (to be confirmed) * Camera Ready Copy: early September 2026 (to be confirmed) Please let us know if you have any questions! Best wishes Achim D. Brucker (University of Exeter) Sebastian Mödersheim (Danmarks Tekniske Universitet) Christoph Sprenger (ETH Zürich) Luca Viganò (King’s College London) -- Prof. Achim Brucker | Chair in Cybersecurity & Head of Group | University of Exeter https://www.brucker.ch | https://logicalhacking.com/blog @adbrucker | @logicalhacking

1 0

PhD Position in Bridging the Gap Between Mathematical Numbers and Software Systems (Deadline: 2026-03-22)
by Achim D. Brucker 10 Mar '26

10 Mar '26

We are seeking an enthusiastic PhD candidate with a strong background in computer science, software engineering, mathematics, or closely related fields. Expertise in formal methods such as program reasoning, programming language semantics, model checking, theorem proving, or computational logic is essential. Mathematical models, e.g., describing physical systems or cryptographic algorithms, rely on ideal numbers. For instance, mathematical integers are infinite and mathematical reals continuous and infinite. Computers work with finite approximations that are bounded (i.e., there is a smallest and largest number) and discrete. This "digital gap" between mathematical models and actual systems is a challenge when implementing safety-critical or security-critical systems: for example, autonomous aircraft or self-driving cars require high-precision representations of their position to avoid collisions. Hence, not considering the approximation of the approximative representation of numbers in computers can result in crashes that can endanger the life of humans. Moreover, many security-critical systems, not limited to cryptographic algorithms, rely on the correct handling of over- and underflows in integer computations. Actually, underflow- and overflow bugs are a root cause for a large number vulnerabilities exploited by cyber security criminal, e.g., for stealing digital currencies worth several billion of dollars. While this is not a new problem (e.g., already in 1982, an float conversion error in a trading systems at the Vancouver Stock Exchange resulted in a loss of several millions of US dollars), an integrated development method preventing such bugs is still not available. This PhD project will address this challenge by developing a rigour approach for developing systems relying on precise representations of numbers, using the interactive theorem prover Isabelle/HOL. The PhD project can focus on 1) the formalisation of concrete representations of machine numbers (e.g., IEEE754, POSIT, Decimal Floating Point, Fixed Point Arithmetic), their (algebraic) properties, and relationship to abstract mathematical numbers; 2) the formalisation and verification of numerical or cryptographic algorithms, establishing a reusable verified library, or 3) the development of an end-to-end refinement approach from mathematical models to machine representations. The PhD will be jointly supervised by Prof. Dr. Achim Brucker (<a.brucker(a)exeter.ac.uk>) and Prof. Dr. Burkhart Wolff (<burkhart.wolff(a)universite-paris-saclay.fr>), leading to a joint degree from the University of Exeter and the University of Paris-Saclay. Information about the programme can be found at * <https://www.exeter.ac.uk/study/pg-research/funding/phdfunding/paris-saclay/> * <https://adum.fr/as/ed/voirproposition.pl?langue=en&matricule_prop=71068&sit…> All applications have to be made via the ADUM system: <https://adum.fr/as/ed/voirproposition.pl?langue=en&matricule_prop=71068&sit…>, latest on the 22nd of March 2026. Best, Achim (and Bukrhart) -- Prof. Achim Brucker | Chair in Cybersecurity & Head of Group | University of Exeter https://www.brucker.ch | https://logicalhacking.com/blog @adbrucker | @logicalhacking

1 0

Call for Participation: Workshop on AI and Theorem Provers in Mathematics (AITPM)
by Achim D. Brucker 10 Mar '26

10 Mar '26

The Workshop on AI and Theorem Provers in Mathematics (AITPM) will explore with leading experts some of the recent developments related to the use of AI and theorem provers in mathematics as well as the perspectives for such future use. - Workshop website: https://aitpm.github.io/ - Venue: Online - Attendance is free. - Registration: https://forms.office.com/e/c7gth3Rb6Q - Date: 8. - 10. April 2026 ## Speakers - Kevin Buzzard (Imperial College) - Minhyong Kim (International Centre for Mathematical Sciences, Edinburgh) - Yang-Hui He (London Institute for Mathematical Sciences) - Paola Iannone (University of Edinburgh) - Shinichi Mochizuki (Research Institute for Mathematical Sciences Kyoto) - Leonardo De Moura (Amazon Web Services) - Lawrence Paulson (University Cambridge) - Chelsea Edmonds (University of Western Australia) - Patrick Massot (University Paris Saclay) ## Programme Schedule (to be confirmed) The preliminary schedule of the workshop is: * April 8th 2026 * 08:00-09:00 Kevin Buzzard * 09:15-10:15 Paola Iannone * 10:45-11:45 Lawrence Paulson * 12:00-13:00 Discussion/panel session * April 9th 2026 * 08:00-09:00 Chelsea Edmond * 09:15-10:15 Yang Hui Heen * 10:45-11:45 Shinichi Mochizuki * 12:00-13:00 Discussion session * April 10th 2026 * 15:00-16:00 Patrick Massot * 16:15-17:15 Leonardo De Moura * 17:45-18:45 Natarajan Shankar (tbc) * 19:00-20:00 Discussion/panel session and closure All times are BST (i.e., London, observing daylight saving time). ## Organisers - Mohamed Saidi (Department of Mathematics and Statistics, University of Exeter) - Barrie Cooper (Department of Mathematics and Statistics, University of Exeter) - Gihan Marasingha (Department of Mathematics and Statistics, University of Exeter) - Achim D. Brucker (Department of Computer Science, University of Exeter) - Diego Marmsoler (Department of Computer Science, University of Exeter) -- Prof. Achim Brucker | Chair in Cybersecurity & Head of Group | University of Exeter https://www.brucker.ch | https://logicalhacking.com/blog @adbrucker | @logicalhacking

1 0

Cabal transitive constraint puzzle
by Viktor Dukhovni 06 Mar '26

06 Mar '26

Dear Cafe and GHC-devs, I am happy to see that Yamamoto-san (cc:d) (the maintainer of the `tls` package) is extending it to include support for MLKEM key agreement. This in turn depends on the `mlkem` library by Olivier Chéron (also many thanks!). Now it turns out that for maximum portability, `mlkem` in turn has a build flag `use_crypton` that selects either `crypton`, or (current default) the older `cryptonite` library as its dependency. So the dependen graph is: tls <- mlkem <- if (use_crypton): crypton else: cryptonite But, at this, point `tls` is crypton-only, and no longer builds with the older cryptonite equivalents. Therefore `tls` adds constraints: mlkem +use_crypton to its `cabal.project` file, which solves the problem for `tls`, but sadly not for any projects that in turn depend on `tls`. To them the constraints in the `cabal.project` file of `tls` are effectively invisible. Since the default flag value in `mlkem` is for now `use_crypton: false`, each project that wants to use the (work-in-progress) `tls` appears to need to explictly know that `tls` requires a non-default build of `mlkem`, and must add the same constraints to its `cabal.project`. That transitive explicit configuration requirement is not something one can reasonably ask projects that depend on `tls to have to add. And of course, more generally, any other such indirect flag-dependent conflict must not become a burden on all consumers of library B that is only compatible with a specific variant of library C. How is this situation supposed to be handled? Is there something in cabal that can automatically convince the solver to select a setting of the `mlkem` flag that is compatible with `tls`? Must `mlkem` be forked instead to be two libraries, one dependent on `cryptonite` and another dependent on `crypton`? I've been unable to find a satisfactory workaround. Any help appreciated. -- Viktor.

6 12

How to unsubscribe?
by Tom Ellis 05 Mar '26

05 Mar '26

Does the footer appear like this to everyone else? _______________________________________________ Haskell-Cafe mailing list -- haskell-cafe(a)haskell.org To (un)subscribe, modify options or view archives go to: Only members subscribed via the mailman list are allowed to post. "go to" where? Does anyone know how to unsubscribe? Thanks, Tom

3 3

Hackage treatment of source code
by Olaf Klinke 02 Mar '26

02 Mar '26

In the past I had no problem with copy & paste from the colorized html that is produced by haddock. Perhaps some browsers/window managers attempt to copy html as html and not plain text, which may obfuscate this experience. As Brandon said, download & unpack the tar.gz linked from a package's main page to obtain the raw source. No need to reach for cabal. Olaf

2 1