Packaging Mathematical Structures
From MaRDI portal
Publication:3183538
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
Related Items
View of Computer Algebra Data from Coq, Computer Certified Efficient Exact Reals in Coq, Theory Presentation Combinators, Automated Reasoning in Higher-Order Regular Algebra, 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
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