halting theorem in nLab

constructive mathematics, realizability, computability

intuitionistic mathematics

propositions as types, proofs as programs, computational trinitarianism

Constructive mathematics

• topos, homotopy topos

• type theory, homotopy type theory

• canonical form, univalence

• Bishop set, h-set

• decidable equality, decidable subset, inhabited set, subsingleton

Realizability

• realizability topos

• realizability model

• realizability interpretation

• effective topos

• Kleene's first algebra, Kleene's second algebra

• function realizability

Computability

• computability

• computation, computational type theory

• computable function, partial recursive function

• computable analysis, constructive analysis

  • Type Two Theory of Effectivity

  • computable function (analysis)

  • exact real computer arithmetic

• computable set

• persistent homology, effective homology

• computable physics

• Church-Turing thesis