Packaging Mathematical Structures
From MaRDI portal
Publication:3183538
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
Related Items
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
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
