Advertisement
Published in:
2014 | OriginalPaper | Chapter
Self Types for Dependently Typed Lambda Encodings
Authors : Peng Fu, Aaron Stump
Published in: Rewriting and Typed Lambda Calculi
Publisher: Springer International Publishing
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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
.