Formalisation of Constructive Univalent Type Theory
There has been in the past 15 years remarkable achievements in the field of interactive theorem proving, both for
checking complex software and checking non trivial mathematical proofs.
For software correctness, X. Leroy (INRIA a...
There has been in the past 15 years remarkable achievements in the field of interactive theorem proving, both for
checking complex software and checking non trivial mathematical proofs.
For software correctness, X. Leroy (INRIA and College de France)
has been leading since 2006 the CompCert project, with a fully verified C compiler.
For mathematical proofs, these systems could handle complex arguments,
such as the proof of the 4 color theorem or the formal proof of Feit-Thompson Theorem
More recently, the Xena project, lead by K. Buzzard, is developing a large library of mathematical facts, and
has been able to help the mathematician P. Scholze (field medalist 2018) to check a highly non trivial proof.
All these examples have been carried out in systems based on the formalism of dependent type theory, and
on early work of the PI. In parallel to these works, also around 15 years ago,
a remarkable and unexpected correspondance was discovered between this formalism
and the abstract study of homotopy theory and higher categorical structures.
A special year 2012-2013 at the Institute of Advance Study (Princeton) was organised by
the late V. Voevodsky (field medalist 2002, Princeton), S. Awodey (CMU) and the PI.
Preliminary results indicate that this research direction is productive,
both for the understanding of dependent type systems and higher category theory, and suggest several crucial
open questions. The objective of this proposal is to analyse these questions, with the ultimate goal
of formulating a new way to look at mathematical objects and potentially a new foundation of mathematics.
This could in turn be crucial for the design of future proof systems able to handle complex highly modular
software systems and mathematical proofs.ver más
02-11-2024:
Generación Fotovolt...
Se ha cerrado la línea de ayuda pública: Subvenciones destinadas al fomento de la generación fotovoltaica en espacios antropizados en Canarias, 2024
01-11-2024:
ENESA
En las últimas 48 horas el Organismo ENESA ha otorgado 6 concesiones
01-11-2024:
FEGA
En las últimas 48 horas el Organismo FEGA ha otorgado 1667 concesiones
Seleccionando "Aceptar todas las cookies" acepta el uso de cookies para ayudarnos a brindarle una mejor experiencia de usuario y para analizar el uso del sitio web. Al hacer clic en "Ajustar tus preferencias" puede elegir qué cookies permitir. Solo las cookies esenciales son necesarias para el correcto funcionamiento de nuestro sitio web y no se pueden rechazar.
Cookie settings
Nuestro sitio web almacena cuatro tipos de cookies. En cualquier momento puede elegir qué cookies acepta y cuáles rechaza. Puede obtener más información sobre qué son las cookies y qué tipos de cookies almacenamos en nuestra Política de cookies.
Son necesarias por razones técnicas. Sin ellas, este sitio web podría no funcionar correctamente.
Son necesarias para una funcionalidad específica en el sitio web. Sin ellos, algunas características pueden estar deshabilitadas.
Nos permite analizar el uso del sitio web y mejorar la experiencia del visitante.
Nos permite personalizar su experiencia y enviarle contenido y ofertas relevantes, en este sitio web y en otros sitios web.