Article ID Journal Published Year Pages File Type
8904286 Annals of Pure and Applied Logic 2018 19 Pages PDF
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
,