Pinned Repositories
camlp5
Preprocessor / Pretty Printer for OCaml
banach_tarski
Formal proof in Coq of Banach-Tarski paradox.
cauchy_schwarz
Formal proof in Coq of Cauchy Schwarz Inequality
coq
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
coq_euler_prod_form
Coq proof of the Euler product formula for the Riemann zeta function (in progress...)
coq_homol_algeb
Homologic Algebra in Coq
coq_real
Real Numbers using LPO
coq_sensitivity
Sensitivity Conjecture in Coq
mlrogue
Rogue written in OCaml
puiseuxth
Formal proof in Coq of Puiseux's Theorem.
roglo's Repositories
roglo/banach_tarski
Formal proof in Coq of Banach-Tarski paradox.
roglo/coq_real
Real Numbers using LPO
roglo/cauchy_schwarz
Formal proof in Coq of Cauchy Schwarz Inequality
roglo/mlrogue
Rogue written in OCaml
roglo/puiseuxth
Formal proof in Coq of Puiseux's Theorem.
roglo/coq_homol_algeb
Homologic Algebra in Coq
roglo/coq_sensitivity
Sensitivity Conjecture in Coq
roglo/coq
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
roglo/coq_euler_prod_form
Coq proof of the Euler product formula for the Riemann zeta function (in progress...)
roglo/coq100
Statement of theorems proven in Coq
roglo/coqtail
roglo/manifesto
Documentation on goals of the coq-community organization, the shared contributing guide and code of conduct.
roglo/mycoqhott
Experiments with HOTT. Trying to implement it in Coq.