Thierry Coquand
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.
| Thierry Coquand | ||
|---|---|---|
.jpg) Thierry Coquand en 2006 | ||
| Información personal | ||
| Nacimiento |
18 de abril de 1961 (63 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 |
| |
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]
Véase también
editarReferencias
editar- ↑ «Thierry Coquand» (en inglés). Universidad de Gotemburgo. Archivado desde el original el 27 de marzo de 2023. Consultado el 27 de marzo de 2023.
- ↑ Constructions: A Higher Order Proof System for Mechanizing Mathematics (en inglés). Abril de 1985. pp. 151-184. ISBN 9783540159834. Consultado el 24 de febrero de 2023.
- ↑ Coquand, Thierry; Huet, Gérard (1985). «A Selected Bibliography on Constructive Mathematics, Intuitionistic Type Theory and Higher Order Deduction». Journal of Symbolic Computation (en inglés) 1 (3): 323-328. doi:10.1016/S0747-7171(85)80040-7. Archivado desde el original el 24 de febrero de 2023. Consultado el 24 de febrero de 2023.
- ↑ «An analysis of Girard's paradox» (en inglés). Archivado desde el original el 24 de febrero de 2023. Consultado el 24 de febrero de 2023.
- ↑ «What is Coq?» (en inglés). Archivado desde el original el 24 de febrero de 2023. Consultado el 24 de febrero de 2023.
- ↑ «Coq received ACM SIGPLAN Programming Languages Software 2013 award» (en inglés). Archivado desde el original el 22 de febrero de 2023. Consultado el 22 de febrero de 2023.
- ↑ «Programming Languages Software Award» (en inglés). Archivado desde el original el 25 de febrero de 2023. Consultado el 25 de febrero de 2023.
- ↑ «Thierry Coquand» (en inglés). Archivado desde el original el 25 de febrero de 2023. Consultado el 25 de febrero de 2023.
- ↑ «Paradoxes and Definitions» (en inglés). Archivado desde el original el 25 de febrero de 2023. Consultado el 25 de febrero de 2023.
Enlaces externos
editar
Datos: Q3524190
Multimedia: Thierry Coquand (computer scientist) / Q3524190
