In this paper, the relationship between the second order typed - calculus 2 and its higher order version is discussed . A purely syntactic proof of the conservativity of over 2 is given.
文摘In this paper, the relationship between the second order typed - calculus 2 and its higher order version is discussed . A purely syntactic proof of the conservativity of over 2 is given.