Journal article
From realizability to induction via dependent intersection
Annals of pure and applied logic, Vol.169(7), pp.637-655
07/2018
DOI: 10.1016/j.apal.2018.03.002
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.
Details
- Title: Subtitle
- From realizability to induction via dependent intersection
- Creators
- Aaron Stump - University of Iowa
- Resource Type
- Journal article
- Publication Details
- Annals of pure and applied logic, Vol.169(7), pp.637-655
- DOI
- 10.1016/j.apal.2018.03.002
- ISSN
- 0168-0072
- eISSN
- 1873-2461
- Publisher
- Elsevier B.V
- Grant note
- DOI: 10.13039/100000001, name: NSF, award: 1524519; DOI: 10.13039/100000005, name: DoD, award: FA9550-16-1-0082
- Language
- English
- Date published
- 07/2018
- Academic Unit
- Computer Science
- Record Identifier
- 9984259479602771
Metrics
19 Record Views