# Contents

## Idea

The Brouwer-Heyting-Kolmogorov interpretation of intuitionistic logic is a description of proofs of propositions in intuitionistic logic as functions, often computable functions?, where it is also called the realizability interpretation.

This is otherwise known as propositions as types and proofs as programs

## References

• Wikipedia, BHK interpretation

• J.-Y. Girard, Proofs and Types

• A. Troelstra, History of Constructivism in the Twentieth Century (1991). (pdf)

• Wouter Pieter Stekelenburg, Realizability Categories (arXiv:1301.2134)

Links to many papers on realizability and related topics may be found here.