There are three files used in this Abella formalization of the proof of totality of the Ackermann relation in muMALL.
This files were proof checked using Abella version 2.0.8.
The best way to read the files above in a browser is to use the following link: ack-proof.html
The formalization first encodes the (parts of the) muMALL proof system. Then there is a proof that given any two natural numbers, the Ackermann relation always yields a third natural number.
Since Abella is not designed to handle muMALL directly, the style of our formalization uses a not-so-typical approach to formalization. In particular, after introducing polarized formulas (muMALL formulas), we introduce a series of axioms in Abella that encode the inference rules of muMALL. Since Abella does not formally allow for the addition of axioms, we simply introduce theorems with no proofs given (using the Abella command skip). Subsequent theorems then state that muMALL sequents (using the ts object-level predicate) are provable from the provided axioms.
An informal description of this proof is given in Section 5 of the paper "Peano Arithmetic and μMALL" by Matteo Manighetti and Dale Miller, https://arxiv.org/abs/2312.13634.