Packaging Mathematical Structures
From MaRDI portal
Recommendations
Cites work
- A constructive algebraic hierarchy in Coq.
- A constructive and formal proof of Lebesgue's dominated convergence theorem in the interactive theorem prover Matita
- A Modular Formalisation of Finite Group Theory
- An introduction to small scale reflection in Coq
- Canonical Big Operators
- Commutative algebra in the Mizar system
- Computing the Wedderburn decomposition of group algebras by the Brauer–Witt theorem
- Defining functions on equivalence classes
- Dependently typed records in type theory
- First-Class Type Classes
- scientific article; zbMATH DE number 1302055 (Why is no real title available?)
- Introduction to algorithms.
- Local Theory Specifications in Isabelle/Isar
- Setoids in type theory
- Telescopic mappings in typed lambda calculus
- Working with Mathematical Structures in Type Theory
Cited in
(46)- A constructive algebraic hierarchy in Coq.
- Automating formalization by statistical and semantic parsing of mathematics
- Experiences from exporting major proof assistant libraries
- Structure-preserving diagram operators
- Modelling algebraic structures and morphisms in ACL2
- scientific article; zbMATH DE number 1670760 (Why is no real title available?)
- Two-Way Automata in Coq
- Theory presentation combinators
- Automated Reasoning in Higher-Order Regular Algebra
- Computational Complexity Via Finite Types
- Formalization of real analysis: a survey of proof assistants and libraries
- scientific article; zbMATH DE number 2089410 (Why is no real title available?)
- 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
- Working with Mathematical Structures in Type Theory
- Canonical Big Operators
- A scalable module system
- scientific article; zbMATH DE number 1927429 (Why is no real title available?)
- Iris from the ground up: a modular foundation for higher-order concurrent separation logic
- Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis
- Validating Mathematical Structures
- Quotients by idempotent functions in Cedille
- A trustful monad for axiomatic reasoning with probability and nondeterminism
- Interfacing Coq + SSReflect with GAP
- Implementation of Bourbaki's \textit{Elements of mathematics} in Coq. II: From natural numbers to real numbers
- Formalization techniques for asymptotic reasoning in classical analysis
- View of computer algebra data from Coq
- Computer Certified Efficient Exact Reals in Coq
- A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading
- Developing the algebraic hierarchy with type classes in Coq
- A formal proof of the irrationality of (3)
- Measure construction by extension in dependent type theory with application to integration
- 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
- Mathematical structures in dependent type theory (invited talk)
- Hierarchy builder: algebraic hierarchies made easy in Coq with Elpi (system description)
- A comprehensive overview of the Lebesgue differentiation theorem in Coq
- A practical formalization of monadic equational reasoning in dependent-type theory
- Use and abuse of instance parameters in the Lean mathematical library.
- Extending equational monadic reasoning with monad transformers
- A unifying logical foundation for initial algebra semantics and induction
- A Unified Framework for Formalizing Matrix Decomposition Proofs
This page was built for publication: Packaging Mathematical Structures
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3183538)
