nLab
Dialectica interpretation

Contents

Contents

Idea

In proof theory, the Dialectica interpretation is a proof interpretation of intuitionistic arithmetic (Heyting arithmetic) into a finite type extension of primitive recursive arithmetic.

References

  • Kurt Gödel, Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes. Dialectica (1958), pp. 280–287.

  • Valeria de Paiva, The Dialectica Categories. University of Cambridge, Computer Laboratory, PhD Thesis, Technical Report 213, (pdf).

Created on November 7, 2018 at 07:08:13. See the history of this page for a list of all contributions to it.