ティエリー・コカン

ティエリー・コカン（フランス語: [kɔkɑ̃] ; 1961年4月18日生まれ）は、フランスのコンピュータ科学者、数学者であり、現在はヨーテボリ大学のコンピュータサイエンスの教授であり、^[1]以前はINRIAに勤務していました。彼は構成的数学、特に構成の計算に関する研究で知られています。

彼は、数学とコンピュータサイエンスの両方の経験を持つもう一人の学者、ジェラール・ユエの指導の下で博士号を取得した。ACMデジタルライブラリによると、彼が最初に発表した論文は、1985年にユエと共同で書いた「構成：数学を機械化する高次の証明システム」である。^[2]コカンとユエはその年の9月に別の共同論文を発表し、構成的数学に関する彼らの考えをさらに展開した。^[3]翌年の1986年、コカンはシステムU論理システムにおけるジラールのパラドックスに関する注目すべき論文を発表した。 ^[4]それ以来、コカンはフランス語と英語の両方でさまざまな論文を執筆している。

理論計算機科学への貢献に加え、コカンはCoq（名前は部分的にコカンの姓に由来する）証明支援ツールの共同作成者としても知られている。Coqは1984年にINRIA（フランスの国立計算機科学数学研究所）で勤務中に開発を開始し、1989年に正式にリリースされた。^[5] Coqは2013年に「機械チェックされた形式推論のインタラクティブな開発のための充実した環境を提供」したとしてACM SIGPLANプログラミング言語ソフトウェア賞を受賞した。 ^[6]^{[7] Coqは数学の問題、特に}四色定理のような調査不可能な証明を持つ問題に対する斬新な解決策を提供するために使用されてきた。また、 CompCert Cコンパイラなどのソフトウェア開発にも使用されている。^[8]

コカンは、ノッティンガム大学のトルステン・アルテンキルヒ教授の研究成果の説明など、自身の専門分野について頻繁に講演を行っている。^[9]

参照

参考文献

^ “Thierry Coquand”.ヨーテボリ大学. 2023年3月27日時点のオリジナルよりアーカイブ。2023年3月27日閲覧。
^ 構成: 数学を機械化する高次の証明システム。1985年4月。pp. 151–184。ISBN 9783540159834. 2023年2月24日時点のオリジナルよりアーカイブ。2023年2月24日閲覧。
^ Coquand, Thierry; Huet, Gérard (1985). 「構成的数学、直観主義型理論、高階演繹に関する選定参考文献」Journal of Symbolic Computation . 1 (3): 323–328. doi :10.1016/S0747-7171(85)80040-7. 2023年2月24日時点のオリジナルよりアーカイブ。 2023年2月24日閲覧。
^ “ジラールのパラドックスの分析”. 2023年2月24日時点のオリジナルよりアーカイブ。2023年2月24日閲覧。
^ “What is Coq?”. 2023年2月24日時点のオリジナルよりアーカイブ。2023年2月24日閲覧。
^ “Coq received ACM SIGPLAN Programming Languages Software 2013 award”. 2023年2月22日時点のオリジナルよりアーカイブ。2023年2月22日閲覧。
^ “Programming Languages Software Award”。2023年2月25日時点のオリジナルよりアーカイブ。2023年2月25日閲覧。
^ “Thierry Coquand”. 2023年2月25日時点のオリジナルよりアーカイブ。2023年2月25日閲覧。
^ 「パラドックスと定義」(PDF)。2023年2月25日時点のオリジナルよりアーカイブ(PDF) 。 2023年2月25日閲覧。

外部リンク

公式ウェブサイト、チャルマーズ
DBLP書誌サーバーの Thierry Coquand

[gu-1] “Thierry Coquand”.ヨーテボリ大学. 2023年3月27日時点のオリジナルよりアーカイブ。2023年3月27日閲覧。

[2] 構成: 数学を機械化する高次の証明システム。1985年4月。pp. 151–184。ISBN 9783540159834. 2023年2月24日時点のオリジナルよりアーカイブ。2023年2月24日閲覧。

[3] Coquand, Thierry; Huet, Gérard (1985). 「構成的数学、直観主義型理論、高階演繹に関する選定参考文献」Journal of Symbolic Computation . 1 (3): 323–328. doi :10.1016/S0747-7171(85)80040-7. 2023年2月24日時点のオリジナルよりアーカイブ。 2023年2月24日閲覧。

[4] “ジラールのパラドックスの分析”. 2023年2月24日時点のオリジナルよりアーカイブ。2023年2月24日閲覧。

[5] “What is Coq?”. 2023年2月24日時点のオリジナルよりアーカイブ。2023年2月24日閲覧。

[6] “Coq received ACM SIGPLAN Programming Languages Software 2013 award”. 2023年2月22日時点のオリジナルよりアーカイブ。2023年2月22日閲覧。

[7] “Programming Languages Software Award”。2023年2月25日時点のオリジナルよりアーカイブ。2023年2月25日閲覧。

[8] “Thierry Coquand”. 2023年2月25日時点のオリジナルよりアーカイブ。2023年2月25日閲覧。

[9] 「パラドックスと定義」(PDF)。2023年2月25日時点のオリジナルよりアーカイブ(PDF) 。 2023年2月25日閲覧。