- Haskell-Cafe - Haskell.org

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 03 Mar '26

03 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

Hackage treatment of source code
by Douglas McIlroy 02 Mar '26

02 Mar '26

Hackage allows one to retrieve "source". However, the so-called source code can't be used, because it is a colorized .html file, not .hs. Even if one wants to use only a snippet of what's on the screen, one must turn to the heavy artillery of Cabal to get it. Can there not be an option to retrieve plain text from Hackage without interposing the colorizer? Doug McIlroy

2 1

Appreciation
by Volker Wysk 01 Mar '26

01 Mar '26

Hi! I've set up my Haskell environment with GHCup and Cabal and compiled a program of mine. It has worked really really well. The developers have my thanks and appreciation. Cheers, Volker

4 4

finding out ghc version from closed issue
by Zoran Bošnjak 28 Feb '26

28 Feb '26

Dear members, I am facing this problem with ghc-9.10.3: https://gitlab.haskell.org/ghc/ghc/-/issues/25477 It looks like the problem is already fixed at some later version. My question is... how do I find out the ghc version from the issue or from the git commit? Zoran

2 1

tls: Hybrid key exchange of ECC and Post-Quantum
by Kazu Yamamoto 27 Feb '26

27 Feb '26

Hello, TLS client of OpenSSL version 3.5 or later specifies hybrid key exchange of ECC and Post-Quantum (such as X25519MLKEM768) and an ECC key exchange (such as X25519) in TLS ClientHello. I have implemented both the hybrid algorithms and the OpenSSL specifying-method in the Haskell "tls" library. Interop with OpenSSL is quite good. I would like to discuss how to specify algorithms in ClientHello before releasing. If you are interested, I would like to invite you to this issue: https://github.com/haskell-tls/hs-tls/issues/516 I thank Olivier Chéron for implementing excellent "mlkem" library. --Kazu

2 2

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

26 Feb '26

Dear all, Registration is now open for the 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