Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Product Trees


view this post on Zulip Email Gateway (Sep 18 2026 at 15:14):

From: Lawrence Paulson <lp15@cam.ac.uk>

I am happy to announce yet another (AI-free!) contribution from the ever-prolific Manuel.

Fast Chinese Remaindering via Product Trees
Manuel Eberl

Product trees are a simple data structure that, broadly speaking, allows dealing with the product of a large number of (typically coprime) integers, or more generally elements of a Euclidean ring.
This is particularly useful for efficient simultaneous modular reduction, i.e. computing for a large number of moduli at the same time for a fixed , and the inverse operation thereof, i.e. modular reconstruction (also known as “Chinese Remaindering”).
The algorithms formalised are adapted from the book “Modern Computer Algebra” by von zur Gathen and Gerhard.

https://isa-afp.org/entries/CRT_Product_Tree.html

Larry


Last updated: Oct 08 2026 at 21:07 UTC