Titlebook: Interactive Theorem Proving; Third International Lennart Beringer,Amy Felty Conference proceedings 2012 Springer-Verlag Berlin Heidelberg

侵蚀

Formalization of Shannon’s Theorems in SSReflect-Coq we produce the first formal proofs of the source coding theorem (that introduces the entropy as the bound for lossless compression), and the direct part of the more difficult channel coding theorem (that introduces the capacity as the bound for reliable communication over a noisy channel).

aggrieve

zonules

安慰

即席演说

A Refinement-Based Approach to Computational Algebra in ,ons on more efficient data structures and linked to their abstract counterparts. We illustrate this methodology on key applications: matrix rank computation, Winograd’s fast matrix product, Karatsuba’s polynomial multiplication, and the gcd of multivariate polynomials.

Hemoptysis

Applying Data Refinement for Monadic Programs to Hopcroft’s Algorithmd, efficient code in various languages, including Standard ML, Haskell and Scala..In order to demonstrate the practical applicability of our framework, we present a verified implementation of Hopcroft’s algorithm for automata minimisation.

真实的你

COKE

A Cantor Trio: Denumerability, the Reals, and the Real Algebraic NumbersThe third proof is of the existence of real transcendental (i.e., non-algebraic) numbers. It also appeared in Cantor’s 1874 paper, as a corollary to the non-denumerability of the reals. What Cantor ingeniously showed is that the algebraic numbers are denumerable, so every open interval must contain at least one transcendental number.

裙带关系

Congruous