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 ι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 ω with positive recursive type definitions, which we analyze. We also prove type preservation for S. © 2014 Springer International Publishing Switzerland.