Packaging Mathematical Structures

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

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

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 subtypingtype inferenceCoqSSReflectformalization of algebra

Mathematics Subject Classification ID

Related Items (31)

Unnamed Item ⋮ Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis ⋮ Validating Mathematical Structures ⋮ Theory Presentation Combinators ⋮ Automated Reasoning in Higher-Order Regular Algebra ⋮ Unnamed Item ⋮ Computational Complexity Via Finite Types ⋮ A scalable module system ⋮ Quotients by Idempotent Functions in Cedille ⋮ Measure construction by extension in dependent type theory with application to integration ⋮ Automating formalization by statistical and semantic parsing of mathematics ⋮ Towards a practical library for monadic equational reasoning in Coq ⋮ Verified correctness, accuracy, and convergence of a stationary iterative linear solver: Jacobi method ⋮ Multiple-inheritance hazards in dependently-typed algebraic hierarchies ⋮ Formalization of real analysis: a survey of proof assistants and libraries ⋮ A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading ⋮ Iris from the ground up: A modular foundation for higher-order concurrent separation logic ⋮ Structure-preserving diagram operators ⋮ A trustful monad for axiomatic reasoning with probability and nondeterminism ⋮ Interfacing Coq + SSReflect with GAP ⋮ View of Computer Algebra Data from Coq ⋮ Computer Certified Efficient Exact Reals in Coq ⋮ 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 ⋮ Two-Way Automata in Coq ⋮ Constructive Formalization of Hybrid Logic with Eventualities ⋮ Experiences from exporting major proof assistant libraries ⋮ Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two, From Natural Numbers to Real Numbers ⋮ Modelling algebraic structures and morphisms in ACL2

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

This page was built for publication: Packaging Mathematical Structures