Thierry Coquand
From Wikipedia, the free encyclopedia
| Thierry Coquand | ||
|---|---|---|
.jpg) Thierry Coquand en 2006 | ||
| Información personal | ||
| Nacimiento |
18 de abril de 1961 (64 años) Isère (Francia) | |
| Nacionalidad | Francesa | |
| Educación | ||
| Educación | doctor en Filosofía | |
| Educado en | Escuela Normal Superior de París | |
| Supervisor doctoral | Gérard Huet | |
| Información profesional | ||
| Ocupación | Matemático, informático teórico e ingeniero | |
| Área | Ciencias de la computación | |
| Empleador | ||
| Obras notables | Coq | |
| Miembro de | Academia Europæa (desde 2011) | |
| Distinciones |
| |
Thierry Coquand (pronunciación en francés: /kɔkɑ̃/; Bourgoin-Jallieu, 18 de abril de 1961) es un informático y matemático francés que actualmente es profesor de informática en la Universidad de Gotemburgo,[1] habiendo trabajado anteriormente en INRIA. Es conocido por su trabajo en matemáticas constructivas, especialmente el cálculo de construcciones.
Recibió su Ph.D. bajo la supervisión de Gérard Huet, otro académico con experiencia tanto en matemáticas como en informática. Según la biblioteca digital ACM, su primer artículo publicado fue una colaboración de 1985 con Huet titulada «Construcciones: un sistema de prueba de orden superior para mecanizar las matemáticas».[2] Coquand y Huet publicaron otro artículo conjunto en septiembre de ese año que amplió aún más sus ideas sobre las matemáticas constructivas.[3] Al año siguiente, 1986, Coquand publicó un artículo notable sobre la paradoja de Girard en el sistema lógico Sistema U.[4] Desde entonces, Coquand ha escrito una amplia variedad de artículos tanto en francés como en inglés.
Además de sus contribuciones a la informática teórica, Coquand también es conocido por ser el cocreador del asistente de prueba Coq (el nombre es en parte una referencia al apellido de Coquand), cuyo desarrollo comenzó en 1984 mientras trabajaba en INRIA (el Instituto Nacional de Investigación de Ciencias de la Computación y Matemáticas de Francia), y que se lanzó oficialmente en 1989.[5] Coq ganó el premio de software de lenguajes de programación SIGPLAN ACM en 2013 por «proporcionar un entorno rico para el desarrollo interactivo del razonamiento formal verificado por máquina».[6][7] Coq se ha utilizado para proporcionar soluciones novedosas para problemas matemáticos, especialmente para aquellos que tienen una prueba no comprobable, como el teorema de los cuatro colores. También se ha utilizado en el desarrollo de software, como con el compilador CompCert C.[8]
Coquand a menudo da charlas sobre los temas en los que se especializa, como su descripción del trabajo del profesor de la Universidad de Nottingham Thorsten Altenkirch.[9]
