Working in a simplicial and constructive context, a new spectral system is defined that relates Serre and Eilenberg–Moore spectral sequences associated to a principal simplicial fibration. The two Eilenberg–Moore spectral sequences (the one where the homology of the fiber is the output, and the other where the homology of the base is computed) are used in our construction. Explicit computer programs are developed, enhancing the Kenzo computer algebra tool to implement that spectral system.

The analysis of digital images using homological procedures is an outstanding topic in the area of Computational Algebraic Topology. In this article, we describe a certified reduction strategy to deal with digital images, but one preserving their homological properties. We stress both the advantages of our approach (mainly, the formalization of the mathematics allowing us to verify the correctness of algorithms) and some limitations (related to the performance of the running systems inside proof assistants). The drawbacks are overcome using techniques that provide an integration of computation and deduction. Our driving application is a problem in bioinformatics, where the accuracy and reliability of computations are specially requested.

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.

Abstract We apply current theorem proving technology to certified code in the domain of abstract algebra. More concretely, based on a formal proof of the Basic Perturbation Lemma (a central result in homological algebra) in the prover Isabelle/HOL, we apply various code generation techniques, which lead to certified implementations of the associated algorithm in ML. In the formal proof, algebraic structures occurring in the Basic Perturbation Lemma are represented in a way, which is not directly amenable to code generation with the available tools. Interestingly, this representation is required in the proof, while for the algorithm simpler data structures are sufficient. Our approach is to establish a link between the non-executable setting of the proof and the executable representation in the algorithm, which is to be generated. This correspondence is established within the logical framework of Isabelle/HOL—that is, it is formally proved correct. The generated code is applied to and illustrated with a number of examples.

In this paper we report on an experience communicating between the GAP computional algebra system (in particular, its HAP package for homological algebra computations) and the Kenzo computer system for Algebraic Topology. Both systems were made to cooperate through an OpenMath link in order to perform computations in group cohomology. Furthermore, once HAP output is integrated into Kenzo, it can be used to compute more complicated algebraic invariants such as the homology groups of various 2-types.

In this paper the analysis of the data structures used in a symbolic computation system, called Kenzo, is undertaken. We deal with the specification of the inheritance relationship since Kenzo is an object-oriented system, written in CLOS, the Common Lisp Object System. We focus on a particular case, namely the relationship between simplicial sets and chain complexes, showing how the order-sorted algebraic specifications formalisms can be adapted, through the “inheritance as coercion” metaphor, in order to model this Kenzo fragment.

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.