Self Types for Dependently Typed Lambda Encodings

ABSTRACT. We revisit lambda encodings of data, proposing new solutions to several old problems, in particular dependent elimination with lambda encodings. We start with a type assignment form of the Calculus of Constructions, restricted recursive definitions and Miquel’s implicit product. We add a type construct \iota x . T, called a self type, which allows T to refer to the subject of typing. We show how the resulting System S with this novel form of dependency supports dependent elimination with lambda encodings, including induction principles. Strong normalization of S is established by defining an erasure from S to a version of F-omega with positive recursive type definitions, which we analyze. We also prove type preservation for S.