Formalizing Double Groupoids and Cross Modules in the Lean Theorem Prover

Lean is a new open source dependently typed theorem prover which is mainly being developed by Leonardo de Moura at Microsoft Research. It is suited to be used for proof irrelevant reasoning as well as for proof relevant formalizations of mathematics. In m

  • PDF / 42,739,945 Bytes
  • 533 Pages / 439.37 x 666.142 pts Page_size
  • 26 Downloads / 176 Views

DOWNLOAD

REPORT

Recommend Documents
The Double Limit Theorem and Its Legacy

146 67 11MB

Formalizing and simulating cross-layer elasticity strategies in Cloud systems

150 25 4MB

Semigroupoids and Groupoids

141 46 532KB

Lazy groupoids

163 15 2MB

Groupoids and the algebra of rewriting in group presentations

155 32 343KB

Generalized Fibonacci sequences in groupoids

170 8 194KB

Formalizing the Shadow Economy in Serbia Policy Measures and Growth

192 106 2MB

Characterizing Deterministic-Prover Zero Knowledge

185 118 14MB

The blenlib and blenkernel Modules

144 75 5MB

Progress in Lean Manufacturing

203 20 2MB

The Completeness Theorem

207 89 3MB

Erratum to: Measurements of top-quark pair differential and double-differential cross-sections in the $$\ell $$

163 100 2MB