Formalization of Constructive Mathematics
(MATHFOR)
Start date: Apr 1, 2010,
End date: Mar 31, 2015
PROJECT
FINISHED
The general theme is to explore the connections between reasoning and computations in mathematics. There are two main research directions. The first research direction is a refomulation of Hilbert's program, using ideas from formal, or pointfree topology. We have shown, with multiple examples, that this allows a partial realization of this program in commutative algebra, and a new way to formulate constructive mathematics. The second research direction explores the computational content using type theory and the Curry-Howard correspondence between proofs and programs. Type theory allows us to represent constructive mathematics in a formal way, and provides key insight for the design of proof systems helping in the analysis of the logical structure of mathematical proofs. The interest of this program is well illustrated by the recent work of G. Gonthier on the formalization of the 4 color theorem.
Get Access to the 1st Network for European Cooperation
Log In
or
Create an account
to see this content
Details
- 100% € 1 912 288,00
-
FP7-IDEAS-ERC
- Project on CORDIS Platform
GOETEBORGS UNIVERSITET
€ 1 912 288,00- Ludde Edgren
- VASAPARKEN 405 30 GOETEBORG (Sweden)