Swedish logician. Well-known in programming languages for his contribution to type theory. In other circles, well-known for an algorithmic definition of randomness.
There is a Wikipedia page on Martin-Löf.
Michael Thompson has undertaken the herculean task of collecting virtually all of Martin-Löf's writings in a GitHub repository.