Point-Free, Set-Free Concrete Linear Algebra
From MaRDI portal
Publication:3088000
DOI10.1007/978-3-642-22863-6_10zbMath1342.68285OpenAlexW3888705MaRDI QIDQ3088000
Publication date: 17 August 2011
Published in: Interactive Theorem Proving (Search for Journal in Brave)
Full work available at URL: https://hal.inria.fr/hal-00805966/file/main.pdf
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (6)
A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem ⋮ Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems ⋮ Certifying standard and stratified Datalog inference engines in SSReflect ⋮ Using abstract stobjs in ACL2 to compute matrix normal forms ⋮ Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL ⋮ A formalization of convex polyhedra based on the simplex method
Uses Software
Cites Work
- Commutative algebra in the Mizar system
- Packaging Mathematical Structures
- A Modular Formalisation of Finite Group Theory
- Canonical Big Operators
- First-Class Type Classes
- Setoids in type theory
- Theorem Proving in Higher Order Logics
- Theorem Proving in Higher Order Logics
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Point-Free, Set-Free Concrete Linear Algebra
