Тьерри Коканд
.jpg)
Тьерри Коканд (англ. Французский: [kɔkɑ̃] ; родился 18 апреля 1961) — французский ученый-компьютерщик и математик, в настоящее время профессор информатики в Гетеборгском университете . [1] ранее работал в ИНРИА . Он известен своими работами в области конструктивной математики , особенно в исчислении конструкций .
Он получил докторскую степень. под руководством Жерара Юэ , еще одного ученого, имеющего опыт работы как в области математики, так и в области информатики. По данным цифровой библиотеки ACM , его первая опубликованная статья была написана в 1985 году в сотрудничестве с Юэ под названием «Конструкции: система доказательств высшего порядка для механизации математики». [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]
См. также [ править ]
Ссылки [ править ]
- ^ «Тьерри Коканд» . Университет Гетеборга . Архивировано из оригинала 27 марта 2023 года . Проверено 27 марта 2023 г.
- ^ Конструкции: система доказательств высшего порядка для механизации математики . Апрель 1985 г., стр. 151–184. ISBN 9783540159834 . Архивировано из оригинала 24 февраля 2023 года . Проверено 24 февраля 2023 г.
- ^ Коканд, Тьерри; Юэ, Жерар (1985). «Избранная библиография по конструктивной математике, интуиционистской теории типов и дедукции высшего порядка» . Журнал символических вычислений . 1 (3): 323–328. дои : 10.1016/S0747-7171(85)80040-7 . Архивировано из оригинала 24 февраля 2023 года . Проверено 24 февраля 2023 г.
- ^ «Анализ парадокса Жирара» . Архивировано из оригинала 24 февраля 2023 года . Проверено 24 февраля 2023 г.
- ^ «Что такое Кок?» . Архивировано из оригинала 24 февраля 2023 года . Проверено 24 февраля 2023 г.
- ^ «Coq получил награду ACM SIGPLAN Programming Languages Software 2013» . Архивировано из оригинала 22 февраля 2023 года . Проверено 22 февраля 2023 г.
- ^ «Награда за программное обеспечение в области языков программирования» . Архивировано из оригинала 25 февраля 2023 года . Проверено 25 февраля 2023 г.
- ^ «Тьерри Коканд» . Архивировано из оригинала 25 февраля 2023 года . Проверено 25 февраля 2023 г.
- ^ «Парадоксы и определения» (PDF) . Архивировано (PDF) из оригинала 25 февраля 2023 года . Проверено 25 февраля 2023 г.
Внешние ссылки [ править ]
- Официальный сайт , Чалмерс
- Тьерри Коканд на DBLP библиографическом сервере
ML- программирование |
|---|
