MATHFOR

Formalization of Constructive Mathematics

Coordinatore	GOETEBORGS UNIVERSITET    more Spiacenti, non ci sono informazioni su questo coordinatore. Contattare Fabio per maggiori infomrazioni, grazie.
Nazionalità Coordinatore	Sweden [SE]
Totale costo	1˙912˙288 €
EC contributo	1˙912˙288 €
Programma	FP7-IDEAS-ERC Specific programme: "Ideas" implementing the Seventh Framework Programme of the European Community for research, technological development and demonstration activities (2007 to 2013)
Code Call	ERC-2009-AdG
Funding Scheme	ERC-AG
Anno di inizio	2010
Periodo (anno-mese-giorno)	2010-04-01   -   2015-03-31

 Partecipanti

#	participant	country	role	EC contrib. [€]
1	GOETEBORGS UNIVERSITET  Organization address address: VASAPARKEN city: GOETEBORG postcode: 405 30 contact info Titolo: Dr. Nome: Ludde Cognome: Edgren Email: send email Telefono: -7862768 Fax: -7864340	SE (GOETEBORG)	hostInstitution	1˙912˙288.00
2	GOETEBORGS UNIVERSITET  Organization address address: VASAPARKEN city: GOETEBORG postcode: 405 30 contact info Titolo: Prof. Nome: Thierry Cognome: Coquand Email: send email Telefono: +46 31-7721030 Fax: +46 31-772 36 63	SE (GOETEBORG)	hostInstitution	1˙912˙288.00

Mappa

 Word cloud

Esplora la "nuvola delle parole (Word Cloud) per avere un'idea di massima del progetto.

 Obiettivo del progetto (Objective)

'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.'