ラッセル 型理論
いまでは、プログラミングに取り入れられている

https://ja.wikipedia.org/wiki/%E5%9E%8B%E7%90%86%E8%AB%96
型理論
型理論（かたりろん、英: Type theory）とは、プログラミング・数学・言語学等に現れる型の概念及びそれらが成す型システムを研究対象とする数学・計算機科学の分野である。特定の型システムのことを型理論と呼ぶこともある。集合論の代替となる数学の基礎として役立てられる型理論（型システム）も存在する。そのような例としてアロンゾ・チャーチの型付きラムダ計算やマルティン・レーフの直観主義型理論が有名である。

https://en.wikipedia.org/wiki/Type_theory
Type theory
Some type theories serve as alternatives to set theory as a foundation of mathematics. Two influential type theories that have been proposed as foundations are:
・Typed λ-calculus of Alonzo Church
・Intuitionistic type theory of Per Martin-Löf
Most computerized proof-writing systems use a type theory for their foundation. A common one is Thierry Coquand's Calculus of Inductive Constructions.

https://en.wikipedia.org/wiki/History_of_type_theory
History of type theory
1900–1927
Origin of Russell's theory of types

1940s–present
Curry–Howard correspondence, 1934–1969
Martin-Löf's Intuitionistic type theory, 1971–1984

Identity Proofs are Not Unique, 1994
This opened up a new area of research, homotopy type theory, where category theory was applied to the identity type.

https://en.wikipedia.org/wiki/Homotopy_type_theory
In mathematical logic and computer science, homotopy type theory (HoTT) refers to various lines of development of intuitionistic type theory, based on the interpretation of types as objects to which the intuition of (abstract) homotopy theory applies.