ペール・マルティン＝レーフ (Per Martin-Löf, 1942年 - ) はスウェーデンの論理学者、哲学者、数学者。直観主義的型理論の創案者として知られる。２００９年までストックホルム大学数学部および哲学部教授を務めた。1964年から1965年にかけてモスクワのアンドレイ・コルモゴロフのもとで学び、ランダム系列に関する研究を行う。1968年から1969年にかけてはシカゴ大学助教授を務め、ここでウィリアム・ハワードとカリー＝ハワード対応に関して議論している。1971年には型理論に関する最初の草稿を書き上げているが、この最初の非可述体系はジャン＝イヴ・ジラールによって矛盾していることが示された（ジラールのパラドックス）。これをきっかけに型理論の概念的基礎の探求へと導かれていったマルティン＝レーフは、1984年の著作で提示した可述型理論を正当化するための証明論的意味論を展開し、またこれに関連していくつかの哲学的著作も発表している。彼の直観主義的型理論は依存型 (dependent type) の概念を発展させたことで知られており、これは後の calculus of construction 等に影響を与えた。また、Nuprl をはじめとして、マルティン＝レーフの型理論に基づいた自動証明システムも開発されている。マルティン＝レーフの業績は今なお論理学および理論計算機科学の研究にインスピレーションを与え続けており、彼のアイデアが持つ可能性はいまだに汲み尽くされていないといえる。

出典:wikipedia