Loading article…
ダミアン・ドリゲスはフランスの学者でありプログラマーである。彼はOCamlシステム、特にそのガベージコレクターの開発者として最もよく知られている。彼はフランス政府の研究機関であるINRIAの研究員（chargé de recherche）である。
1990年、DoligezとXavier Leroyは、高速な逐次ガベージコレクタを備えたバイトコードインタープリタに基づくCamlの実装（Caml Lightと呼ばれる）を構築し、並行処理のサポートを追加して拡張し始めました。[ 2 ] 1996年、DoligezはOCamlの最初のバージョンを構築したチームの一員であり、[ 3 ]それ以来（2023年4月現在）、この言語のコアメンテナーを務めています。[ 4 ]
1994年、ハル・フィニーはサイファーパンクのメーリングリストで暗号化されたSSLv2セッションを解読するという挑戦状を出した[ 5 ] 。ドリゲスはInria、ENS、エコール・ポリテクニークの予備のコンピュータを使って、8日間で鍵空間の半分をスキャンした後、それを解読した[ 6 ]。彼はコンテストで僅差の2位となり、優勝チームはわずか2時間前に結果を発表した[ 7 ] [ 8 ] 。
2006年以来、Doligezは等号を含む一階古典論理のための定理証明器Zenon [ 9 ] を共同開発してきました。Zenonは、認証済みプログラムを設計・開発できるプログラミング環境Focalize [ 11 ]を駆動するエンジン[ 10 ]です。この環境は、オブジェクト指向機能を備えた関数型言語に基づいており、プログラマーはコードの形式仕様と証明を同じ環境で記述できます。証明生成はZenonを使用して支援され、結果はRocq証明チェッカーを使用して形式的に機械検証されます。
2008年、DoligezはLeslie Lamportらと協力し、階層構造のコンピュータ支援証明の段階的な開発と検証をサポートするTLA+証明マネージャを構築した。[ 12 ]この証明マネージャプロジェクトは2022年現在も活発に維持・開発されている。[ 13 ]