本記事は、Göteborg大学のNordströmらによる『Martin-Löf型理論によるプログラミング』の概要紹介です。この書籍は、直観主義的論理と型理論に基づくプログラミング手法を解説しており、形式的証明や構成的論理に興味のある読者に向けられています。1990年に出版され、現在はオンラインで無料公開されています。