Thierry Coquand -Thierry Coquand

Coquand v roce 2006

Thierry Coquand ( francouzsky:  [kɔkɑ̃] ; narozen 18. dubna 1961 v Bourgoin-Jallieu ) je francouzský počítačový vědec a matematik, který je v současné době profesorem informatiky na univerzitě v Göteborgu , předtím pracoval na INRIA . Je známý svou prací v konstruktivní matematice , zejména v počtu konstrukcí .

Získal titul Ph.D. pod dohledem Gérarda Hueta , dalšího akademika, který má zkušenosti jak v matematice, tak v informatice. Podle ACM Digital Library byl jeho první publikovaný článek ve spolupráci s Huetem z roku 1985 s názvem „Konstrukce: Systém důkazů vyššího řádu pro mechanizaci matematiky“. Coquand a Huet publikovali v září téhož roku další společný článek, který dále rozšířil jejich myšlenky týkající se konstruktivní matematiky. V následujícím roce, 1986, Coquand publikoval pozoruhodný článek o Girardově paradoxu v logickém systému System U. Od té doby Coquand napsal širokou škálu prací ve francouzštině i angličtině.

Kromě svých příspěvků k teoretické informatice je Coquand také známý tím, že je spolutvůrcem Coq ( jméno je částečně odkazem na Coquandovo příjmení) důkazového asistenta, jehož vývoj začal v roce 1984, když pracoval ve společnosti INRIA (a Francouzský národní výzkumný ústav pro informatiku a matematiku), který byl oficiálně uveden na trh v roce 1989. Coq získal v roce 2013 cenu ACM SIGPLAN Programming Languages ​​Software Award za „poskytování bohatého prostředí pro interaktivní vývoj strojově kontrolovaného formálního uvažování“ . Coq byl používán poskytovat nová řešení pro matematické problémy, obzvláště pro ty, které mají non-surveyable důkaz , takový jako čtyři teorém barvy . Byl také použit při vývoji softwaru, například s kompilátorem CompCert C.

Coquand často přednáší o předmětech, na které se specializuje, jako je jeho popis práce profesora Thorstena Altenkircha z University of Nottingham .

Viz také

Reference

externí odkazy