Cocan, Thierry
| Thierry Cocán | |
|---|---|
| Thierry Coquand | |
| Fecha de nacimiento | 18 de abril de 1961 [1] (61 años) |
| Lugar de nacimiento | Jalieu (Francia, departamento de Isère) |
| País | Francia |
| Esfera científica | Fundamentos de las matemáticas , informática teórica |
| Lugar de trabajo | Universidad de Gotemburgo |
| alma mater | Escuela Normal Superior (París) |
| Titulo academico | Doctor |
| Título académico | Profesor |
| consejero científico | Gerard Hue |
| Conocido como | Desarrollador de cálculo de construcción, coorganizador del programa de fundamentos univalentes de las matemáticas, investigador de topología sin sentido |
| Premios y premios | Premio de Investigación de la Sociedad Gödel (2008) |
| Archivos multimedia en Wikimedia Commons | |
Thierry Coquand ( fr. Thierry Coquand ; nacido el 18 de abril de 1961 ) es un matemático francés , especialista en teoría de tipos y demostración automática , creador del cálculo de construcción , coorganizador del programa para la creación de fundamentos univalentes de las matemáticas . Profesor de la Facultad de Informática e Ingeniería de la Universidad de Gotemburgo .
Biografía
Nacido en Jalieu ( departamento de Isère ). En 1980 se graduó de la Escuela Normal Superior de París , en 1982 aprobó la "agregación matemática" ( fr. agrégation de mathématiques ) - un examen competitivo para el derecho a enseñar matemáticas en las escuelas secundarias. En 1985 defendió su tesis doctoral ( PhD ) en informática en INRIA bajo la supervisión de Gerard Huet . En 1985-1989 fue investigador visitante en INRIA, en 1989 se desempeñó como director de investigación ( fr. directeur de recherche ).
Desde 1990 vive y trabaja en Suecia : fue investigador visitante en la Universidad Tecnológica de Chalmers , y desde 1996 es profesor en la Universidad de Gotemburgo .
Trabajos científicos
Mientras trabajaba con Gérard Huet a mediados de la década de 1980, desarrolló el cálculo de construcción , un cálculo λ polimórfico de orden superior con tipos dependientes que ocupa el punto más alto en el cubo λ de Barendregt y luego se convirtió en la base del software de prueba automática Coq . sistema _ (El nombre "Coq" oculta tanto el acrónimo de cálculo de construcción, CoC , como la primera parte del apellido de Kokan).
Principales publicaciones sobre teoría de tipos y demostración automática. Una serie de trabajos de las décadas de 1990 y 2000 está dedicada a la topología sin sentido y al álgebra constructiva .
Actividad organizativa
Miembro del comité de programa del XIV Congreso Internacional de Lógica, Metodología y Filosofía (2011, Nancy ).
Junto con Vladimir Voevodsky y Steve Awodey , coorganizó un programa especial de investigación para el año académico 2012-2013 en el Instituto de Estudios Avanzados , dedicado a los fundamentos univalentes de las matemáticas , en cuyo marco participó en la creación conjunta del libro “Teoría de los tipos homotópicos: Fundamentos univalentes de las matemáticas”, en el que se exponen los principales resultados del programa.
Miembro de los consejos editoriales de las revistas Journal of Functional Programming y Mathematical Structures in Computer Science (ambas publicadas por Cambridge University Press ). Revisor de libros sobre álgebra constructiva y teoría de la demostración para Springer-Verlag y Princeton University Press .
Premios y comunidades
En 2008, ganó un importante premio de investigación de la Sociedad Gödel ( Sociedad inglesa de Kurt Gödel ) por su trabajo sobre espacios de metrizaciones ( Espacio inglés de valoraciones ) [2] .
En 2011 fue elegido miembro de la Sociedad Real de Ciencias y Letras de Gotemburgo ( en sueco: Kungliga Vetenskaps- och Vitterhetssamhället i Göteborg ).
Principales publicaciones
- Thierry Coquand. Un análisis de la paradoja de Girard (inglés) // Symposium on Logic in Computer Science (LIS'86), Cambridge, MA, 1986. - Cambridge, MA : IEEE , 1986. - P. 227-236 . — análisis de un análogo de la paradoja de Burali-Forti para la teoría intuicionista de los tipos de Martin-Löf .
- Thierry Coquand, Gerard Huet. El cálculo de construcciones (Español) // Información y Computación . - 1988. - vol. 76 , núm. 2-3 . - P. 95-120 . — ISSN 0890-5401 . - doi : 10.1016/0890-5401(88)90005-3 . — la publicación principal sobre el cálculo de estructuras.
- Thierry Coquand. Una semántica de evidencia para la lógica clásica (inglés) // Journal of Symbolic Logic . - 1995. - vol. 60 , núm. 1 . - P. 325-337 . — ISSN 0022-4812 . -doi : 10.2307/ 2275524 . .
- Thierry Coquand. Sur un théorème de Kronecker concernant les variétés algébriques (fr.) // Comptes rendus hebdomadaires des séances de l'Académie des sciences . - París, 2004. - Vol. 338 , n º 4 . — págs. 291–294 . — ISSN 0001-4036 . -doi : 10.1016/ j.crma.2003.12.008 .
- Thierry Coquand. Teoría de tipos // Enciclopedia de Filosofía de Stanford . - Stanford : Stanford University Publishing, 2010. - Artículo sobre teoría de tipos en la Enciclopedia de Filosofía de Stanford .
Notas
- ↑ Biblioteca Nacional Alemana, Biblioteca Estatal de Berlín, Biblioteca Estatal de Baviera , Registro de la Biblioteca Nacional de Austria #122538900 // Control Regulador General (GND) - 2012-2016.
- ↑ Åsa Ekvall. Thierry Coquand ha sido galardonado con la beca del Premio de Investigación del Centenario Kurt Gödel . Universidad de Gotemburgo (6 de abril de 2008). Recuperado: 1 de marzo de 2014.
Enlaces
- Página de inicio de Thierry Cocan (inglés) . Recuperado: 1 de marzo de 2014.
 sitios temáticos | ||||
|---|---|---|---|---|
| ||||