Project Page Index Table of Contents
    • Continuity
  • Axioms for synthetic computability
    • Synthetic Church's thesis
  • Halting problems
    • Constructions
  • Kleene trees
    • Omniscience principles as axioms on trees
    • WKL
    • WKL equivalences
  • CT in relation to other axioms
    • Provable choice axioms
    • Extensionality axioms
    • Classical logical axioms
    • Axioms of russian constructivism
    • Choice axioms
    • Brouwer's intuitionism
  • Halting problem for the call-by-value lambda-calculus HaltL
    • Finite types
    • Infinite types and predicates
  • Decidability and Enumerability
    • Decidability
      • Discrete types
    • Enumerability
      • Enumerable types
    • List enumerability
    • Definitions
    • Pre-order properties
    • Semi-decidability
  • Propositional truth table reductions
  • Bounded Turing reductions
  • Turing reductions
  • Bauer's Turing reductions
  • Reducibility
    • Many-one reducibility
    • One-one reducibility
    • Truth-table reducibility
    • Total Turing reducibility
Generated by coqdoc and improved with CoqdocJS