scientific article; zbMATH DE number 1424016

MaRDI QIDQ4945205zbMATH OpenFDO

Authors Venanzio Capretta

Publication date 23 March 2000

zbMATH Keywords

universal algebratheory of typesautomated reasoning about general algebraic structuresproof development system Coq

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Algebraic structures (08A99) Software, source code, etc. for problems pertaining to general algebraic systems (08-04)

Cited in

(10)

• Formalizing in Coq Hidden Algebras to Specify Symbolic Computation Systems
• Formalization of universal algebra in Agda
• Structure-preserving diagram operators
• On the relationship between compact regularity and Gentzen's cut rule
• Computer theorem proving in mathematics
• A Type of Partial Recursive Functions
• Injective types in univalent mathematics
• Reasoning About Algebraic Structures with Implicit Carriers in Isabelle/HOL
• On the collection of points of a formal space
• Modelling algebraic structures and morphisms in ACL2

Describes a project that uses

Uses Software

• Coq

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4945205)