stringtranslate.com

Thierry Coquand

Coquand en 2006

Thierry Coquand ( en francés: [kɔkɑ̃] ; nacido el 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 el INRIA . Es conocido por su trabajo en matemáticas constructivas , especialmente el cálculo de construcciones .

Recibió su doctorado bajo la supervisión de Gérard Huet , otro académico que tiene 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 "Constructions: A Higher Order Proof System for Mechanizing Mathematics". [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 System 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 pruebas Coq (el nombre es en parte una referencia al apellido de Coquand), que comenzó a desarrollar en 1984 mientras trabajaba en INRIA (un instituto nacional francés de investigación en informática y matemáticas), y que se lanzó oficialmente en 1989. [5] Coq ganó el premio ACM SIGPLAN Programming Languages ​​Software Award en 2013, por "proporcionar un entorno rico para el desarrollo interactivo de razonamiento formal controlado 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 encuestable , 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

Referencias

  1. ^ "Thierry Coquand". Universidad de Gotemburgo . Archivado desde el original el 27 de marzo de 2023. Consultado el 27 de marzo de 2023 .
  2. ^ Construcciones: Un sistema de prueba de orden superior para mecanizar las matemáticas. Abril de 1985. Págs. 151-184. ISBN 9783540159834Archivado desde el original el 24 de febrero de 2023 . Consultado el 24 de febrero de 2023 .
  3. ^ Coquand, Thierry; Huet, Gérard (1985). "Una bibliografía seleccionada sobre matemáticas constructivas, teoría de tipos intuicionista y deducción de orden superior". Journal of Symbolic Computation . 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álisis de la paradoja de Girard". Archivado desde el original el 24 de febrero de 2023. Consultado el 24 de febrero de 2023 .
  5. ^ "¿Qué es Coq?". Archivado desde el original el 24 de febrero de 2023. Consultado el 24 de febrero de 2023 .
  6. ^ "Coq recibió el premio ACM SIGPLAN Programming Languages ​​Software 2013". Archivado desde el original el 22 de febrero de 2023. Consultado el 22 de febrero de 2023 .
  7. ^ "Premio de Lenguajes de Programación de Software". Archivado desde el original el 25 de febrero de 2023. Consultado el 25 de febrero de 2023 .
  8. ^ "Thierry Coquand". Archivado desde el original el 25 de febrero de 2023. Consultado el 25 de febrero de 2023 .
  9. ^ "Paradojas y definiciones" (PDF) . Archivado (PDF) del original el 25 de febrero de 2023 . Consultado el 25 de febrero de 2023 .

Enlaces externos