Certified symbolic manipulation is an emerging new field where programs are accompanied by certificates that, suitably interpreted, ensure the correctness of the algorithms. In this paper, we focus on algebraic algorithms implemented in the proof assistant ACL2, which allows us to verify correctness in the same programming environment. The case study is that of bivariate simplicial polynomials, a data structure used to help the proof of properties in Simplicial Topology. Simplicial polynomials can be computationally interpreted in two ways. As symbolic expressions, they can be handled algorithmically, increasing the automation in ACL2 proofs. As representations of functional operators, they help proving properties of categorical morphisms. As an application of this second view, we present the definition in ACL2 of some morphisms involved in the Eilenberg-Zilber reduction, a central part of the Kenzo computer algebra system. We have proved the ACL2 implementations are correct and tested that they get the same results as Kenzo does.

III t.his papor t.he aua.lysis of t.lie data struct,ures uwd in 21 software systcn1 for SyIuhOlic Clomput.at,ioI1 in Algrlxdc T0l>010g~, ~IIOWU i1S EAT (Ejfedi~~~ Al,~~ehic T'o~o~o~TJ), is undertalwn.Having tho11ght.Of t.lIe rolr: Of fIIIIct.ionalIJ~Ograuming in this particular prograru, we 11ilVC come to a generitl rlcfinit,ion of an operation on .\lJstractData.1'ylJw: froIII XI abst~a(~t, &l.ta type 'T il I~CW a.hstract tli1t.at,yl>r 'TI,~,~, is COIlStrUCtPd.which SllOUld br consitlercd iLS tlJ1' iLhSt.rMt,dilt,?I type Of tlle iItIpleIIICI1t.i1tiOIJSOf 7. Tllen n'c ljrovc t.llilt the tla.ta strwtur(!sused in EAT in? irIlple~licril.;lti(,IIR of il.bSt.I'iWt.diit il tJ?W 7, rrl,, (SO th!);arc' "i~iil)lcIilcIltiltiolis sqiiarcd" ).In adtlit.ion~tlicy arc: in a sense, tlir most.genera.ln-e cm obtain: siucc they are fiual ohjccbs in rcrtain cabegorics of irnl)lenieIit,ations.