A Formal Proof of the Computation of Hermite Normal Form in a General Setting (Q6108811): Difference between revisions

@@ Property / cites work @@
+Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm
+Normal rank
@@ Property / cites work @@
+A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem
+Normal rank
@@ Property / cites work @@
+Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
+Normal rank
@@ Property / cites work @@
+Locales: a module system for mathematical theories
+Normal rank
@@ Property / cites work @@
+Algorithms for Hermite and Smith Normal Matrices and Linear Diophantine Equations
+Normal rank
@@ Property / cites work @@
+Formalized linear algebra over Elementary Divisor Rings in Coq
+Normal rank
@@ Property / cites work @@
+Refinements for Free!
@@ Property / cites work: Refinements for Free! / rank @@
+Normal rank
@@ Property / cites work @@
+Q3139838
@@ Property / cites work: Q3139838 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5195247
@@ Property / cites work: Q5195247 / rank @@
+Normal rank
@@ Property / cites work @@
+The Misfortunes of a Trio of Mathematicians Using Computer Algebra Systems. Can We Trust in Them?
+Normal rank
@@ Property / cites work @@
+Q5302559
@@ Property / cites work: Q5302559 / rank @@
+Normal rank
@@ Property / cites work @@
+A Rigorous Subexponential Algorithm For Computation of Class Groups
+Normal rank
@@ Property / cites work @@
+The HOL Light theory of Euclidean space
@@ Property / cites work: The HOL Light theory of Euclidean space / rank @@
+Normal rank
@@ Property / cites work @@
+Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
+Normal rank
@@ Property / cites work @@
+An application of the Hermite normal form in integer programming
+Normal rank
@@ Property / cites work @@
+Fast Parallel Computation of Hermite and Smith Forms of Polynomial Matrices
+Normal rank
@@ Property / cites work @@
+Polynomial Algorithms for Computing the Smith and Hermite Normal Forms of an Integer Matrix
+Normal rank
@@ Property / cites work @@
+From Types to Sets by Local Type Definitions in Higher-Order Logic
+Normal rank
@@ Property / cites work @@
+Using abstract stobjs in ACL2 to compute matrix normal forms
+Normal rank
@@ Property / cites work @@
+A decision algorithm for linear sentences on a PFM
+Normal rank
@@ Property / cites work @@
+Verifying a Compiler for Java Threads
@@ Property / cites work: Verifying a Compiler for Java Threads / rank @@
+Normal rank
@@ Property / cites work @@
+Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems
+Normal rank
@@ Property / cites work @@
+Q5668937
@@ Property / cites work: Q5668937 / rank @@
+Normal rank
@@ Property / cites work @@
+Isabelle/HOL. A proof assistant for higher-order logic
+Normal rank
@@ Property / cites work @@
+Flyspeck II: The basic linear programs
@@ Property / cites work: Flyspeck II: The basic linear programs / rank @@
+Normal rank
@@ Property / cites work @@
+A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle
+Normal rank
@@ Property / cites work @@
+Beyond unimodular transformations
@@ Property / cites work: Beyond unimodular transformations / rank @@
+Normal rank
@@ Property / cites work @@
+Commutative algebra in the Mizar system
@@ Property / cites work: Commutative algebra in the Mizar system / rank @@
+Normal rank
@@ links / mardi / name / links / mardi / name @@
+Publication:6108811