Kenzo

swMATH4861MaRDI QIDQ17016FDOQ17016

Author name not available (Why is that?)

Described by source

• Towards Constructive Homological Algebra in Type Theory

Cited In (68)

• Formalizing in Coq Hidden Algebras to Specify Symbolic Computation Systems
• Derived functors of nonadditive functors and homotopy theory
• Using Open Mathematical Documents to Interface Computer Algebra and Proof Assistant Systems
• A new Kenzo module for computing the Eilenberg-Moore spectral sequence
• A formalization of the Smith normal form in higher-order logic
• fKenzo: a user interface for computations in algebraic topology
• Modeling inheritance as coercion in a symbolic computation system
• A certified reduction strategy for homological image processing
• Incidence simplicial matrices formalized in Coq/SSReflect
• Computing the homology of groups: the geometric way.
• Computational homotopy of finite regular CW-spaces
• Effective homotopy of fibrations
• Homological models for semidirect products of finitely generated Abelian groups.
• Searching high order invariants in computer imagery
• Topology of arrangements and representation stability. Abstracts from the workshop held January 14--20, 2018
• Certified symbolic manipulation: bivariate simplicial polynomials
• Computing the first stages of the Bousfield-Kan spectral sequence
• Homotopy groups as centers of finitely presented groups.
• Statistics for data with geometric structure. Abstracts from the workshop held January 21--27, 2018
• A system for computing and reasoning in algebraic topology
• Constructive algebraic topology
• Effective computation of generalized spectral sequences
• Computing multipersistence by means of spectral systems
• A case study of \(A_{\infty}\)-structure
• A computational approach of \(A_{\infty }\)-(co)algebras
• A Mathematica notebook for computing the homology of iterated products of groups.
• Calculating cocyclic Hadamard matrices in Mathematica: exhaustive and heuristic searches
• Effective spectral systems relating Serre and Eilenberg-Moore spectral sequences
• A parameterization process: from a functorial point of view
• Computing in Coq with infinite algebraic data structures
• Proving with ACL2 the correctness of simplicial sets in the Kenzo system
• Applying ACL2 to the formalization of algebraic topology: simplicial polynomials
• Computing invariants for multipersistence via spectral systems and effective homology
• Computing higher Leray-Serre spectral sequences of towers of fibrations
• Mediated Access to Symbolic Computation Systems
• Formalization of a normalization theorem in simplicial topology
• Object oriented institutions to specify symbolic computation systems
• Effective homology of bicomplexes, formalized in Coq
• Homotopical and combinatorial aspects of the theory of normal series in groups.
• A mechanized proof of the basic perturbation lemma
• Triangulations of complex projective spaces
• Title not available (Why is that?)
• Generating certified code from formal proofs: a case study in homological algebra
• A Bousfield-Kan algorithm for computing the \textit{effective} homotopy of a space
• Interoperating between computer algebra systems: computing homology of groups with Kenzo and GAP
• Homotopy groups of suspended classifying spaces: an experimental approach
• Effective homological computations on finite topological spaces
• On homotopy groups of the suspended classifying spaces
• Algebraic models for homotopy types
• Homology computation during an incremental construction process
• Simplicial monoid actions and associated monoid constructions
• Verifying the bridge between simplicial topology and algebra: the Eilenberg-Zilber algorithm
• Modelling algebraic structures and morphisms in ACL2
• Title not available (Why is that?)
• A combinatorial tool for computing the effective homotopy of iterated loop spaces
• Title not available (Why is that?)
• An axiomatic setup for algorithmic homological algebra and an alternative approach to localization
• Verifying an algorithm computing discrete vector fields for digital imaging
• ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System
• An implementation of effective homotopy of fibrations
• Computing with locally effective matrices
• Computing spectral sequences
• Monomial resolutions for efficient computation of simplicial homology
• A case-study in algebraic manipulation using mechanized reasoning tools
• A Kenzo interface for algebraic topology computations in SageMath
• Computational Science – ICCS 2005
• Integrating Multiple Sources to Answer Questions in Algebraic Topology
• Title not available (Why is that?)

This page was built for software: Kenzo