| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 8904286 | Annals of Pure and Applied Logic | 2018 | 19 Pages |
Abstract
In this paper, it is shown that induction is derivable in a type-assignment formulation of the second-order dependent type theory λP2, extended with the implicit product type of Miquel, dependent intersection type of Kopylov, and a built-in equality type. The crucial idea is to use dependent intersections to internalize a result of Leivant's showing that Church-encoded data may be seen as realizing their own type correctness statements, under the Curry-Howard isomorphism.
Related Topics
Physical Sciences and Engineering
Mathematics
Logic
Authors
Aaron Stump,