马丁-洛夫（Martin-Löf，1942—），瑞典逻辑学家、数理统计学家和哲学家。

马丁-洛夫还是一个业余的鸟类观测家，他发表的第一篇科学论文即是关于鸟类迁徙活动中存活率的统计学研究。

在1964年到1965年间，马丁-洛夫曾在莫斯科大学学习，师从柯尔莫哥洛夫。在1966年发表的论文On the definition of random sequences中，他首次给出随机序列的确切定义，后来的算法信息论将所谓“随机字符串”定义为一个不能够被任何短于该字符串的计算机程序生成的字符串，即一个柯氏复杂性不小于自身长度的字符串。由此，算法信息论第一次明确地将“随机”和“非随机”、借由计算模型中的概念区分开了。

马丁-洛夫开创的直觉类型论提出了依赖类型的概念，直接启发了构造演算（CoC）与LF逻辑框架的建立。一些流行的计算机证明系统和程序语言在此基础上得以开发，包括：Coq、Agda、NuPRL、LEGO、Twelf 和 Epigram等。

参考文献：

https://zh.wikipedia.org/zh-cn/佩尔·马丁-洛夫