デール・ミラー（学者）

ミラーとゴパラン・ナダトゥールは、高階直観主義論理に基づいた論理プログラミング言語λPrologを共同開発しました。λPrologは、λツリー構文（高階抽象構文とも呼ばれる）を直接サポートした最初のプログラミング言語でした。1985年の言語の発表以来、ELPIやTeyjusなど、さまざまな実装が行われてきました。^{[ 12 ]}

ミラーはアルウェン・ティウと共に、不動点と一階述語論理の量化の証明理論を拡張し、λツリー構文を取り入れた。彼らの分析によると、失敗としての否定は、一般量化と全称量化の区別を強制する。彼らは一般量化子を捉えるために∇量化子を導入した。彼らの拡張された論理システムは、π計算の多くのモデル検査とメタ理論的側面を直接捉えることができた。^{[ 13 ]}

ミラーは、ナダトゥール、ティウ、アンドリュー・ガセック、カウストゥフ・チャウドリと共同で、対話型定理証明器Abellaの設計に貢献した。この証明器はλツリー構文を直接サポートしているため、束縛を含む構文オブジェクトに対して帰納的および共帰納的に推論することが可能である。この証明器は、 λ計算、π計算の形式化されたメタ理論、および操作的意味論を用いて指定されたプログラミング言語にうまく適用されている。^{[ 1 ]}

ミラーは計算論理と証明論の研究を行っており、特に証明論の概念をコンピュータサイエンスの問題に応用することに重点を置いている。彼は、証明論が古典論理、直観主義論理、線形論理における論理プログラミングの有益な基盤を提供できることを示した。^{[ 14 ]}チャック・リャンと共同で、彼は集中シーケント計算証明の概念の開発に貢献した。この特定のスタイルの証明システムは、彼が2012年に受賞したERCアドバンスドグラントであるProofCertの基礎として使用され、幅広い証明証明書フォーマットを定義してすぐに実装することができた。^{[ 15 ]}

ミラーはコンピュータサイエンスの分野でも線形論理を利用してきた。特に、自然言語解析、操作的意味仕様、モデル検査、古典論理、直観主義論理、線形論理の証明システムの仕様への線形論理の応用を実証している。^{[ 16 ]}

ミラーはまた、λ計算式の統一についても書いており、特に、存在量化子と全称量化子の両方の下で行われる統一の扱いと、高階統一のパターン統一断片の特定に焦点を当てている。この断片は、λ変換の通常の規則で束縛子を扱いながら、一階統一に非常によく似ている。^{[ 17 ]}

• Miller, D. & Nadathur, G. (2012)プログラミング高階論理、ISBN 9780521879408、ケンブリッジ大学出版局。

• ミラー、D. (2025)証明理論と論理プログラミング - 証明探索としての計算、ISBN 9781009561280、ケンブリッジ大学出版局。

• Nadathur, G., & Miller, D. (1988). λPrologの概要. 第5回国際論理プログラミング会議, 810–827.
• ミラー、D. (1989). 論理プログラミングにおけるモジュールの論理分析.論理プログラミングジャーナル、6(1-2)、79–108.
• Miller, D., Nadathur, G., Pfenning, F., & Scedrov, A. (1991). 論理プログラミングの基礎としての統一証明. Annals of Pure and Applied logic, 51(1-2), 125–157.
• ミラー、D. (1991). ラムダ抽象、関数変数、および単純な単一化を備えた論理プログラミング言語。論理と計算ジャーナル、1(4)、497–536。
• ミラー、D. (1992). 混合接頭辞の下での統一. 記号計算ジャーナル、14(4)、321–358.
• Hodas, JS、および Miller, D. (1994)。直観主義線形論理の断片における論理プログラミング。Information and Computation、110(2)、327–365。
• Miller, D., & Tiu, A. (2005). 一般的な判断のための証明理論. ACM Transactions on Computational Logic, 6(4), 749–783.
• Liang, C. & Miller, D. (2009). 線形論理、直観主義論理、古典論理における焦点化と偏極化. Theoretical Computer Science, 410(46), 4747–4768.
• Gacek, A.、Miller, D.、Nadathur, G. (2011). 名目上の抽象化. Information and Computation 209(1), 48–73.
• Chihani, Z., Miller, D., & Renaud, F. (2017). 証明証拠のための意味論的フレームワーク。自動推論ジャーナル。59(3) 287–330。
• ミラー、D. (2022). 論理プログラミングの証明論的基礎に関する概説. 論理プログラミングの理論と実践, 22(6), 859–904.