Packaging Mathematical Structures

DOI10.1007/978-3-642-03359-9_23zbMath1252.68253MaRDI QIDQ3183538

Assia Mahboubi, François Garillot, Laurence Rideau, Georges Gonthier

Publication date: 20 October 2009

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

Full work available at URL: https://doi.org/10.1007/978-3-642-03359-9_23

zbMATH Keywords

coercive subtyping; type inference; Coq; SSReflect; formalization of algebra

Mathematics Subject Classification ID

Related Items

Interfacing Coq + SSReflect with GAP, View of Computer Algebra Data from Coq, Computer Certified Efficient Exact Reals in Coq, A scalable module system, Modelling algebraic structures and morphisms in ACL2, Theory Presentation Combinators, Automated Reasoning in Higher-Order Regular Algebra, Computational Complexity Via Finite Types, Point-Free, Set-Free Concrete Linear Algebra, Formal proofs for theoretical properties of Newton's method, Type classes for mathematics in type theory, A pluralist approach to the formalisation of mathematics, Constructive Formalization of Hybrid Logic with Eventualities

Uses Software

• Coq
• Mizar
• Matita
• Coq/SSReflect

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Commutative algebra in the Mizar system
• Dependently typed records in type theory
• Telescopic mappings in typed lambda calculus
• A constructive algebraic hierarchy in Coq.
• Computing the Wedderburn decomposition of group algebras by the Brauer–Witt theorem
• Working with Mathematical Structures in Type Theory
• A Modular Formalisation of Finite Group Theory
• Canonical Big Operators
• First-Class Type Classes
• Local Theory Specifications in Isabelle/Isar
• Setoids in type theory
• Defining functions on equivalence classes