The Kenzo team of la Universidad de la Rioja obtained
"The Distinguished Software Demonstration Award" at the Issac 2019 Meeting, Beijing.
Their presentation is
web reachable; after having reached this link, wait for some environment downnloading;
when the standard Jupyter page is displayed, click the RISE button, the last one of the Jupyter
toolbar. Full screen by F11.
Also, work in progress by Gerd Heber (HDF Group) to make Kenzo easily loadable
from and compatible with any Common Lisp system. Already usable. If interested, see the
corresponding Jupyter page, reachable by any GitHub user.
Overview.
The Kenzo program implements the methods of Constructive Algebraic
Topology. The funny corresponding acronym CAT gave the idea to name
this program as my beloved cat.
The first version of this program, called EAT for Effective Algebraic
Topology, was a joint work with Julio Rubio (1990). The EAT program was
totally rewritten with Xavier Dousson in 1998, becoming Kenzo, on the one hand
to include many technical improvements, in particular in memory management,
improvements deduced from the EAT experience, and on the other hand to
implement the Whitehead Tower and compute homotopy groups of
arbitrary simply connected simplicial sets, the heart of Xavier's thesis. A detailed Kenzo documentation was simulatneously written by Yvon
Siret.
The 1.1.8 version now proposed takes account of the new mathematical
technology based on Discrete Vector Fields. Discovered by Robin Forman, it happens this method
considerably improves the implementation of the EilenbergZilber theorem,
twisted or not, and also the computation of the effective homology of
the EilenbergMacLane spaces, crucial when using the Postnikov or Whitehead
towers.
Examples of results obtained thanks to the Kenzo program.

In the paper:
Roman Mikhailov, Jie Wu
On homotopy groups of the suspended classifying spaces
Algebraic & Geometric Topology, 2010, vol.10, pp.565–625.
the authors state in Theorem 5.4:
Let \(A_4\) be the 4th alternating group. Then
\(\pi_4(\Sigma K(A_4,1)) = \mathbf{Z}/4\), with \(K(A_4,1)\) being the
corresponding EilenbergMacLane space, and \(\Sigma\) the suspension functor.
The elementary method used by the Kenzo program, known as the Whitehead
tower, produces a different result, namely \(\pi_4(\Sigma K(A_4,1))
= \mathbf{Z}/12\). The authors of the quoted paper inadvertently forgot the
3primary component. This Kenzo computation was done by Ana Romero, using
extramodules devoted to group resolutions written by herself.

The Kenzo program is now used for an application in Neurology, for
automatic counting of synapses in snapshots of neurons. See this webpage.
Other examples of results reachable by Kenzo:
 Let \(P\mathbf{R}\) (resp. \(P^n\mathbf{R}\)) the infinite real projective space
(resp. the \(n\)dimensional real projective space). Then Kenzo has
determined the groups
H_{i}(\Omega^{2}(PR/P^{2}R);Z) for i < 8. This
computation has been at the origin of an interesting paper by Vladimir
Smirnov determining the whole Z_{2}homology of
the iterated loop spaces of the truncated projective spaces (tex, dvi, ps: only the ps version contains the appendix
but in a bad format because of TeX problems).
 The Kenzo program has also determined the homotopy groups
π_{i}(PR/P^{2}R) for i < 8. These computations have
motivated a nice work
(dvi, ps)
by Fred Cohen and Ran Levi, who go much further with other related
spaces.
 The field where Kenzo seems at this time the most in advance is
with the spaces whose TeX notation is Y = \Omega^{k} (X)
\cup_{2} D^{p}, where X is a simplicial set beginning in
dimension n=p+k1 with a H_{n} = Z; a pcell is attached to a loop
space of X by a map of degree 2. Kenzo can compute the first homology groups
of the first loop spaces of Y and also its first homotopy groups. For
example H_{i}(\Omega(\Omega(S^{3}) \cup_{2}
D^{3})) is computed by Kenzo for i < 10.
 The longest Kenzo computation. Consists in
playing the following game:

Take the stunted real projective space P4 =
P^{∞}(R)/P^{3}(R).

Construct the loop space OP4 = Ω(P4). It is easy to prove the homotopy
group π_{3}(OP4) = Z.

Attaching a 4disk e^{4} to OP4 by a map S^{3} → OP4 of
degree 4 makes sense and products a new space DOP4.

Construct the loop space ODOP4 = Ω(DOP4). It is easy to proof
π_{2}(ODOP4) = Z/4Z.

Attaching a 3disk e^{3} to ODOP4 by a map S^{2} → ODOP4
of degree 2 makes sense and products a new space X = DODOP4.

Construct the loop space OX = ODODOP4 = Ω(DODOP4).

Exercise: Compute the first homology
groups of OX = ODODOP4.
The Kenzo program spent almost exactly two
months to compute H_{i}(OX) for i ≤ 7. The space OX is quite
artificial, not so complicated but designed to accumulate some known
difficulties: the space P4 is not a suspension; the influence of attaching a
disk by a nontrivial attaching map before looping is a difficult subject, so
far without algorithmic solution; the loop functor is applied three times.
The point is that most topologists think a spectral sequence is an algorithm
computing the desired homology groups and this example is designed to convince
them there is in fact some essential gap; they are invited to propose an
algorithm computing these homology groups through the usual
EilenbergMoore spectral sequence; even a "theoretical" algorithm would be
enough, we do not think the exact value of these groups has much
interest…
On the contrary, the methods of effective homology allow the user to
design an algorithm computing the effective homology of a loop space
when the effective homology of the initial space is given. And the ordinary
homology is a byproduct of effective homology. So that the recipe is: starting
from the effective homology of the initial space, here P4, therefore trivial,
compute the effective homology of the intermediate spaces, and when the final
space is reached, you can deduce the ordinary homology groups.
Results:

H_{0}(OX) = Z.

H_{1}(OX) = Z/2Z.

H_{2}(OX) = (Z/2Z)^{2} + Z.

H_{3}(OX) = (Z/2Z)^{4} + Z/8Z.

H_{4}(OX) = (Z/2Z)^{10} + Z/4Z + Z^{2}.

H_{5}(OX) = (Z/2Z)^{23} + Z/8Z + Z/16Z.

H_{6}(OX) = (Z/2Z)^{52} + (Z/4Z)^{3} + Z^{3}

H_{7}(OX) = (Z/2Z)^{113} + Z/4Z + (Z/8Z)^{3} + Z/16Z + Z/32Z + Z

[December 2020] The Kenzo program constructs and
uses an extra garbage collector for the specific results computed by the
program. Changing the parameters of this garbage collector dramatically
improved the computing speed. For example the last result H_{7}(OX) is
now obtained in 40 minutes.
Kenzo extensions.
A Kenzo extension deserves to be signalled: written by Ana Romero, it gives a
complete description of the Serre and EilenbergMoore spectral sequences when
versions with homology effective are known for the initial spaces. See Ana Romero's paper, now published in JSC.
Ana Romero also wrote various new Kenzomodules devoted to some methods
allowing her to compute the effective homology of some groups and so to obtain for example
the first homotopy groups π_{k}SBG for some simple noncommutative groups G.
Work in progress.
You can be interested by this small Kenzodemonstration
file.
See also the Barcelona demonstration given in
the 3rd European Congress of Mathematics.
The detailed Kenzo documentation (340 p.) was
written by Yvon Siret in 19989. Yvon Siret was not a topologist, he was "only"
(?!) a (very good) computer scientist, who learned Algebraic Topology when
writing this document. His advices were also often crucial when writing down
the source code. Many thanks to him!
Previous various compressed archives (tgz, tar and zip) have been replaced by
this unique 7zip version, usable under Linux and Windows as well, much more
compact! In particular, the previous Kenzodoc.pdf component, nonsearchable,
has been replaced by another equal (!) version available elsewhere, searchable.
Thanks to Marek Kaluba for the notification.
Before the Kenzo program (1998), the EAT program was written in 1990 by Julio
Rubio and FS. It was the first program ever written implementing spectral
sequences, in fact only some particular cases of the EilenbergMoore spectral
sequence. The goal was the computation of the first homology groups of some
loop spaces, for which no algorithm was previously concretely available. An
implementation rather primitive, just designed to illustrate our methods of
Effective Homology by a concrete experimental program.
The EAT program is also studied by logicians and computer scientists. Those
possibly interested can download the EATprogram
and its documentation.