realizability

Realizability is a method that can be used to produce models of logic from a model of computation.

Examples include (in historical order):

• Kleene realizability, using Turing machines (or natural numbers through an enumeration of said machines)
• Kreisel realizability, also called modified realizability using typed lambda-calculus, which is slightly more convenient
• Dialectica, which introduces a sort of notion of "counter proof"
• classical realizability, also called Krivine realizability, allowing to create model of classical logics
• linear realizability, sometimes abusively called transcendantal syntax or Geometry of Interaction, (based on the program where it originated), used to create models of linear logic

There are also categorical pendants of these construction, called glueing constructions.

Finally, these are deeply related to logical relations.