Cut-Elimination: Experiments with CERES. - Matthias Baaz; Stefan Hetzl; Alexander Leitsch; Clemens Richter; Hendrik Spohr (LPAR, 2004)

Proof Transformation by CERES. - Matthias Baaz; Stefan Hetzl; Alexander Leitsch; Clemens Richter; Hendrik Spohr (MKM, 2006)

CERES: An analysis of Fürstenberg's proof of the infinity of primes. - Matthias Baaz; Stefan Hetzl; Alexander Leitsch; Clemens Richter; Hendrik Spohr (Theor. Comput. Sci., 2008)