Thierry Cocán | |
---|---|
Thierry Coquand | |
Fecha de nacimiento | 18 de abril de 1961 [1] (61 años) |
Lugar de nacimiento | Jalieu (Francia, departamento de Isère) |
País | Francia |
Esfera científica | Fundamentos de las matemáticas , informática teórica |
Lugar de trabajo | Universidad de Gotemburgo |
alma mater | Escuela Normal Superior (París) |
Titulo academico | Doctor |
Título académico | Profesor |
consejero científico | Gerard Hue |
Conocido como | Desarrollador de cálculo de construcción, coorganizador del programa de fundamentos univalentes de las matemáticas, investigador de topología sin sentido |
Premios y premios | Premio de Investigación de la Sociedad Gödel (2008) |
Archivos multimedia en Wikimedia Commons |
Thierry Coquand ( fr. Thierry Coquand ; nacido el 18 de abril de 1961 ) es un matemático francés , especialista en teoría de tipos y demostración automática , creador del cálculo de construcción , coorganizador del programa para la creación de fundamentos univalentes de las matemáticas . Profesor de la Facultad de Informática e Ingeniería de la Universidad de Gotemburgo .
Nacido en Jalieu ( departamento de Isère ). En 1980 se graduó de la Escuela Normal Superior de París , en 1982 aprobó la "agregación matemática" ( fr. agrégation de mathématiques ) - un examen competitivo para el derecho a enseñar matemáticas en las escuelas secundarias. En 1985 defendió su tesis doctoral ( PhD ) en informática en INRIA bajo la supervisión de Gerard Huet . En 1985-1989 fue investigador visitante en INRIA, en 1989 se desempeñó como director de investigación ( fr. directeur de recherche ).
Desde 1990 vive y trabaja en Suecia : fue investigador visitante en la Universidad Tecnológica de Chalmers , y desde 1996 es profesor en la Universidad de Gotemburgo .
Mientras trabajaba con Gérard Huet a mediados de la década de 1980, desarrolló el cálculo de construcción , un cálculo λ polimórfico de orden superior con tipos dependientes que ocupa el punto más alto en el cubo λ de Barendregt y luego se convirtió en la base del software de prueba automática Coq . sistema _ (El nombre "Coq" oculta tanto el acrónimo de cálculo de construcción, CoC , como la primera parte del apellido de Kokan).
Principales publicaciones sobre teoría de tipos y demostración automática. Una serie de trabajos de las décadas de 1990 y 2000 está dedicada a la topología sin sentido y al álgebra constructiva .
Miembro del comité de programa del XIV Congreso Internacional de Lógica, Metodología y Filosofía (2011, Nancy ).
Junto con Vladimir Voevodsky y Steve Awodey , coorganizó un programa especial de investigación para el año académico 2012-2013 en el Instituto de Estudios Avanzados , dedicado a los fundamentos univalentes de las matemáticas , en cuyo marco participó en la creación conjunta del libro “Teoría de los tipos homotópicos: Fundamentos univalentes de las matemáticas”, en el que se exponen los principales resultados del programa.
Miembro de los consejos editoriales de las revistas Journal of Functional Programming y Mathematical Structures in Computer Science (ambas publicadas por Cambridge University Press ). Revisor de libros sobre álgebra constructiva y teoría de la demostración para Springer-Verlag y Princeton University Press .
En 2008, ganó un importante premio de investigación de la Sociedad Gödel ( Sociedad inglesa de Kurt Gödel ) por su trabajo sobre espacios de metrizaciones ( Espacio inglés de valoraciones ) [2] .
En 2011 fue elegido miembro de la Sociedad Real de Ciencias y Letras de Gotemburgo ( en sueco: Kungliga Vetenskaps- och Vitterhetssamhället i Göteborg ).
sitios temáticos | ||||
---|---|---|---|---|
|