• Intuitionistic Type Theory
• Constructive Mathematics
• Brouwer–Heyting–Kolmogorov interpretation
  • the standard explanation of intuitionistic logic
• Realizability
• Heyting arithmetic