Universal algebra in type theory

DOI10.1007/3-540-48256-3_10MaRDI QIDQ4945205zbMATH OpenFDO

Authors Venanzio Capretta

Publication date 23 March 2000

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-48256-3_10

zbMATH Keywords

automated reasoning about general algebraic structuresproof development system Coqtheory of typesuniversal algebra

Mathematics Subject Classification ID

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

Review text

Formalizing universal algebra within the theory of types by means of the proof development system Coq, the author sets up a framework for automated reasoning about general algebraic structures. For the entire collection see [Zbl 0929.00038].

Cited in

(12)

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

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Universal algebra in type theory

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