Book chapter
Self Types for Dependently Typed Lambda Encodings
Rewriting and Typed Lambda Calculi, pp.224-239
Lecture Notes in Computer Science, Springer International Publishing
2014
DOI: 10.1007/978-3-319-08918-8_16
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.
Details
- Title: Subtitle
- Self Types for Dependently Typed Lambda Encodings
- Creators
- Peng Fu - University of IowaAaron Stump - University of Iowa
- Resource Type
- Book chapter
- Publication Details
- Rewriting and Typed Lambda Calculi, pp.224-239
- Publisher
- Springer International Publishing; Cham
- Series
- Lecture Notes in Computer Science
- DOI
- 10.1007/978-3-319-08918-8_16
- eISSN
- 1611-3349
- ISSN
- 0302-9743
- Language
- English
- Date published
- 2014
- Academic Unit
- Computer Science
- Record Identifier
- 9984259501702771
Metrics
6 Record Views