Abstract

In this paper we describe the Curry-Howard-De Bruijn isomorphism between Higher Order Many Sorted Intuitionistic Predicate Logic PREDω and the type system λPREDω, which can be considered a subsystem of the Calculus of Constructions. The type system is presented using the concept of a Pure Type System, which is a very elegant framework for describing type systems. We show in great detail how formulae and proof trees of the logic relate to types and terms of the type system, respectively. Finally, we discuss some consequences of the isomorphism with respect to the relation between the systems discussed in this paper