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]