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

Thierry Coquand en 2006
Información personal
Nacimiento 18 de abril de 1961 Ver y modificar los datos en Wikidata (63 años)
Isère (Francia) Ver y modificar los datos en Wikidata
Nacionalidad Francesa
Educación
Educación doctor en Filosofía Ver y modificar los datos en Wikidata
Educado en Escuela Normal Superior de París Ver y modificar los datos en Wikidata
Supervisor doctoral Gérard Huet Ver y modificar los datos en Wikidata
Información profesional
Ocupación Matemático, informático teórico e ingeniero Ver y modificar los datos en Wikidata
Área Ciencias de la computación Ver y modificar los datos en Wikidata
Empleador
Obras notables Coq Ver y modificar los datos en Wikidata
Miembro de Academia Europæa (desde 2011) Ver y modificar los datos en Wikidata
Distinciones
  • ACM Software System Award (2013) Ver y modificar los datos en Wikidata

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

editar

Referencias

editar
  1. «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. 
  2. 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. 
  3. 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. 
  4. «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. 
  5. «What is Coq?» (en inglés). Archivado desde el original el 24 de febrero de 2023. Consultado el 24 de febrero de 2023. 
  6. «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. 
  7. «Programming Languages Software Award» (en inglés). Archivado desde el original el 25 de febrero de 2023. Consultado el 25 de febrero de 2023. 
  8. «Thierry Coquand» (en inglés). Archivado desde el original el 25 de febrero de 2023. Consultado el 25 de febrero de 2023. 
  9. «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