13 citations · 24 across the 2 of their papers we have counts for
2 papers
cs.LO2016★ 13 cited
Formalized linear algebra over Elementary Divisor Rings in Coq
Guillaume Cano, Cyril Cohen, Maxime Dénès +2
This paper presents a Coq formalization of linear algebra over elementary divisor rings, that is, rings where every matrix is equivalent to a matrix in Smith normal form. The main…
cs.PL2014★ 11 cited
Testing Noninterference, Quickly
Catalin Hritcu, Leonidas Lampropoulos, Antal Spector-Zabusky +5
Information-flow control mechanisms are difficult both to design and to prove correct. To reduce the time wasted on doomed proof attempts due to broken definitions, we advocate mod…