EAT
EAT: symbolic software for effective homology computation. Kenzo: EAT (= Effective Algebraic Topology), the previous program. 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 Eilenberg-Moore 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 EAT-program and its documentation.
Keywords for this software
References in zbMATH (referenced in 17 articles )
Showing results 1 to 17 of 17.
Sorted by year (- Heras, Jónathan; Martín-Mateos, Francisco Jesús; Pascual, Vico: Modelling algebraic structures and morphisms in ACL2 (2015)
- Domínguez, César; Duval, Dominique: A parameterization process: from a functorial point of view (2012)
- Lambán, Laureano; Martín-Mateos, Francisco-Jesús; Rubio, Julio; Ruiz-Reina, José-Luis: Formalization of a normalization theorem in simplicial topology (2012)
- Domínguez, César; Rubio, Julio: Effective homology of bicomplexes, formalized in Coq (2011)
- Heras, Jónathan; Pascual, Vico; Rubio, Julio: Proving with ACL2 the correctness of simplicial sets in the Kenzo system (2011)
- Aransay, J.; Domínguez, C.: A case-study in algebraic manipulation using mechanized reasoning tools (2010)
- Aransay, Jesús; Ballarin, Clemens; Rubio, Julio: Generating certified code from formal proofs: a case study in homological algebra (2010)
- Domínguez, César; Duval, Dominique: Diagrammatic logic applied to a parameterisation process (2010)
- Martín-Mateos, Francisco-Jesus; Rubio, Julio; Ruiz-Reina, Jose-Luis: ACL2 verification of simplicial degeneracy programs in the Kenzo system (2009)
- Heras, Jónathan; Pascual, Vico; Rubio, Julio: Mediated access to symbolic computation systems (2008)
- Andrés, Mirian; Lambán, Laureano; Rubio, Julio: Executing in Common Lisp, proving in ACL2 (2007)
- Domínguez, César; Lambán, Laureano; Rubio, Julio: Object oriented institutions to specify symbolic computation systems (2007)
- Aransay, Jesús; Ballarin, Clemens; Rubio, Julio: Extracting computer algebra programs from statements (2005)
- Aransay, Jesús; Ballarin, Clemens; Rubio, Julio: Four approaches to automated reasoning with differential algebraic structures (2004)
- Lambán, Laureano; Pascual, Vico; Rubio, Julio: An object-oriented interpretation of the EAT system (2003)
- Domínguez, César; Lambán, Laureano; Pascual, Vico; Rubio, Julio: Hidden specification of a functional system (2001)
- Domínguez, César; Lambán, Laureano; Pascual, Vico; Rubio, Julio: Institutions: mathematics for computer specification (2001)