| An induction principle for Pure Type Systems (1998) | |||||||||||||||
Abstract | |||||||||||||||
| We present an induction principle for Pure Type Systems and use that principle to dene 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 [12] and Barthe, Hatclioe and S#rensen [6], which have been respectively used to dene j-long normal forms and CPS translations for the systems of Barendregt's-cube [2, 3]. 1 | |||||||||||||||
Details der Publikation | |||||||||||||||
| |||||||||||||||