A constructive algebraic hierarchy in Coq.

DOI10.1006/jsco.2002.0552zbMath1038.68108OpenAlexW2013140497MaRDI QIDQ1404425

Herman Geuvers, Randy Pollack, Jan Zwanenburg, Freek Wiedijk

Publication date: 21 August 2003

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL: http://hdl.handle.net/2066/104042

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Mechanization of proofs and logical operations (03B35)

Related Items

Mechanizing complemented lattices within Mizar type system, Validating Mathematical Structures, Invariants for the FoCaL language, Packaging Mathematical Structures, Integration of multiple formal matrix models in Coq, Effective homology of bicomplexes, formalized in Coq, Semigroups with apartness, Organizing numerical theories using axiomatic type classes, Finite Groups Representation Theory with Coq, Type classes for mathematics in type theory, Formalization of ring theory in PVS. Isomorphism theorems, principal, prime and maximal ideals, Chinese remainder theorem, Theory of Constructive Semigroups with Apartness – Foundations, Development and Practice, Modelling algebraic structures and morphisms in ACL2

Uses Software

• AXIOM
• Coq
• PVS

Cites Work

• Ergänzung zu einer Arbeit von Hellmuth Kneser über den Fundamentalsatz der Algebra
• Coercive subtyping
• Implicit coercions in type systems
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item