We introduce a general purpose typed λ-calculus λ∞ which contains intuitionistic logic, is capable of internalizing its own derivations as λ-terms and yet enjoys strong normalization with respect to a natural reduction system. In particular, λ∞ subsumes the typed λ-calculus. The Curry-Howard isomorphism converting intuitionistic proofs into λ∞terms is a simple instance of the internalization property of λ∞. The standard semantics of λ∞ is given by a proof system with proof checking capacities. The system λ∞ is a theoretical prototype of reflective extensions of a broad class of type-based systems in programming languages, provers, AI and knowledge representation, etc.