A cartesian closed category in Martin-Löf s intuitionistic type theory

Silvio Valentini. A cartesian closed category in Martin-Löf s intuitionistic type theory. Theoretical Computer Science, 290(1):189-219, 2003.

Abstract

Abstract is missing.