Coqtail
COQ Theorems, Abstractions and Implementations (Bachelor-Level)
News
[2012-03-12] Proof of Lagrange's four-square theorem.
[2011-08-26] Talks @ Coq workshop on a constructive axiomatics for ℝ and resolution of differential equations using reflection
[2011-07-31] Talk @ THedu on Coq with power series.
[2010-2011] COQTAIL is now a junior lab funded by the ENS Lyon.
Origin & Objectives
The COQTAIL project is the biological son of the workpackage ‘Proofs’ of the COQUILLE project. It is therefore based on all the results obtained during the development of COQUILLE.
In addition to implementing tools dedicated to the easy formalization of mathematics as we see them in french Classes préparatoires, this project will proove Bachelor-level results.
Development axes
- Analysis (real and complex)
- Arithmetic
- Calculability
- ℂ implementation
- Logic and ℝ axiomatic expressivity
- Topology
