.jpg/1280px-Thierry_Coquand_(cropped).jpg)
Тьерри Коканд ( фр . Thierry Coquand ; родился 18 апреля 1961 г.) — французский учёный-компьютерщик и математик, в настоящее время профессор компьютерных наук в Гётеборгском университете [1] , ранее работавший в INRIA . Он известен своими работами в области конструктивной математики , особенно исчисления конструкций .
Он получил докторскую степень под руководством Жерара Юэ , другого ученого, имеющего опыт как в математике, так и в информатике. Согласно ACM Digital Library , его первой опубликованной статьей была совместная работа с Юэ в 1985 году под названием «Constructions: A Higher Order Proof System for Mechanizing Mathematics» (Конструкции: система доказательств высшего порядка для механизации математики). [2] Коканд и Юэ опубликовали еще одну совместную статью в сентябре того же года, в которой они еще больше развили свои идеи относительно конструктивной математики. [3] В следующем, 1986 году, Коканд опубликовал заслуживающую внимания статью о парадоксе Жирара в логической системе System U. [4] С тех пор Коканд написал множество статей как на французском, так и на английском языках.
В дополнение к его вкладу в теоретическую информатику, Кокванд также известен как соавтор помощника по доказательству Coq (название частично является ссылкой на фамилию Кокванда), разработку которого он начал в 1984 году, работая в INRIA (французский национальный исследовательский институт компьютерных наук и математики), и который был официально выпущен в 1989 году. [5] Coq выиграл премию ACM SIGPLAN Programming Languages Software Award в 2013 году за «предоставление богатой среды для интерактивной разработки проверяемых машиной формальных рассуждений». [6] [7] Coq использовался для предоставления новых решений математических задач, особенно для тех, которые имеют не поддающееся проверке доказательство , например, теорема о четырех красках . Он также использовался в разработке программного обеспечения, например, с компилятором CompCert C. [8]
Кокванд часто выступает с докладами по темам, в которых он специализируется, например, он описывает работу профессора Ноттингемского университета Торстена Альтенкирха . [9]