Title: An Induction Principle for Pure Type Systems Authors: Gilles Barthe, John Hatcliff, Morten Heine Soerensen Source: Theoretical Computer Science We present an induction principle for Pure Type Systems and use that principle to define CPS translations and to solve the problem of Expansion Postponement for a large class of Pure Type Systems. Our principle strengthens and generalises similar principles by Dowek, Huet and Werner and the present authors, which have been respectively used to define eta-long normal forms and CPS translations for the systems of Barendregt's lambda-cube.