Kenzo

swMATH4861MaRDI QIDQ17016FDOQ17016

Author name not available (Why is that?)

Described by source

• Towards Constructive Homological Algebra in Type Theory

Cited In (68)

• 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?)
• Formalizing in Coq Hidden Algebras to Specify Symbolic Computation Systems
• Derived functors of nonadditive functors and homotopy theory
• Homology Computation During an Incremental Construction Process
• Using Open Mathematical Documents to Interface Computer Algebra and Proof Assistant Systems
• Homotopy groups as centres of finitely presented groups
• A new Kenzo module for computing the Eilenberg-Moore spectral sequence
• Computing Multipersistence by Means of Spectral Systems
• Effective Computation of Generalized Spectral Sequences
• A formalization of the Smith normal form in higher-order logic
• fKenzo: a user interface for computations in algebraic topology
• A System for Computing and Reasoning in Algebraic Topology
• Modeling inheritance as coercion in a symbolic computation system
• Verifying an Algorithm Computing Discrete Vector Fields for Digital Imaging
• Computing the homology of groups: the geometric way.
• AN AXIOMATIC SETUP FOR ALGORITHMIC HOMOLOGICAL ALGEBRA AND AN ALTERNATIVE APPROACH TO LOCALIZATION
• A Mathematica Notebook for Computing the Homology of Iterated Products of Groups
• Calculating Cocyclic Hadamard Matrices in Mathematica: Exhaustive and Heuristic Searches
• 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
• Computing the first stages of the Bousfield-Kan spectral sequence
• Title not available (Why is that?)
• Statistics for data with geometric structure. Abstracts from the workshop held January 21--27, 2018
• A Certified Reduction Strategy for Homological Image Processing
• Homotopy groups of suspended classifying spaces: An experimental approach
• Constructive algebraic topology
• Effective spectral systems relating Serre and Eilenberg-Moore spectral sequences
• A parameterization process: from a functorial point of view
• 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
• Certified symbolic manipulation
• 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
• 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
• Effective homological computations on finite topological spaces
• On homotopy groups of the suspended classifying spaces
• Algebraic models for homotopy types
• Simplicial monoid actions and associated monoid constructions
• Verifying the bridge between simplicial topology and algebra: the Eilenberg-Zilber algorithm
• Proving with ACL2 the Correctness of Simplicial Sets in the Kenzo System
• Modelling algebraic structures and morphisms in ACL2
• Applying ACL2 to the Formalization of Algebraic Topology: Simplicial Polynomials
• Incidence Simplicial Matrices Formalized in Coq/SSReflect
• Title not available (Why is that?)
• A combinatorial tool for computing the effective homotopy of iterated loop spaces
• Title not available (Why is that?)
• A case study of 𝐴_∞-structure
• A computational approach ofA_∞-(co)algebras
• Computing in Coq with Infinite Algebraic Data Structures
• 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

This page was built for software: Kenzo